Commands

Generated on: Tue Sep 19 17:10:07 CEST 2017by gendoc.groovy.

Covering the proof script commands of KeY.

assume

Synopsis: assume <TERM>

The assume command is an unsound taclet rule and takes one argument:

The command adds the formula passed as argument to the antecedent a formula #2 to which the command is applied

Arguments:

auto

Synopsis: auto [all=<BOOLEAN>] [steps=<INT>]

Arguments:

cut

Synopsis: cut <TERM>

Arguments:

exit

Synopsis: exit

Arguments:

focus

Synopsis: focus <SEQUENT>

Arguments:

instantiate

Synopsis: instantiate formula=<TERM> var=<STRING> occ=<INT> with=<TERM>

Arguments:

javascript

Synopsis: javascript <STRING>

Arguments:

leave

Synopsis: leave

Arguments:

let

Synopsis: let

Arguments:

macro

Synopsis: macro <STRING>

Arguments:

rule

Synopsis: rule <STRING> [on=<TERM>] [formula=<TERM>] [occ=<INT>] [inst_=<TERM>]

Arguments:

schemaVar

Synopsis: schemaVar <STRING> <STRING>

Arguments:

script

Synopsis: script <STRING>

Arguments:

select

Synopsis: select formula=<TERM>

Arguments:

set

Synopsis: set [oss=<BOOLEAN>] [=<STRING>]

Arguments:

skip

Synopsis: skip

Arguments:

smt

Synopsis: smt solver=<STRING>

Arguments:

tryclose

Synopsis: tryclose steps=<INTEGER> <STRING>

Arguments: