| java.lang.Object
 de.uka.ilkd.key.proof.examples.BuildProofForTrue
| BuildProofForTrue | | public class BuildProofForTrue (Code) | | The
BuildProofForTrue.run method of this class will construct a proof object
for the sequent that has the formula true in the succedent.
It then prints out the proof and its list of open goals.
|
| buildBuiltInRuleIndex | | public BuiltInRuleIndex buildBuiltInRuleIndex()(Code) | | Return an empty built-in rule index
|
| buildFormula | | public Term buildFormula()(Code) | | Return the formula true
|
| buildInitialProof | | public Proof buildInitialProof()(Code) | | return the proof for the constructed sequent.
|
| buildRuleAppIndex | | public RuleAppIndex buildRuleAppIndex()(Code) | | Return a RuleAppIndex appropriate for our rules.
|
| buildSequent | | public Sequent buildSequent()(Code) | | return a sequent containing the formula true.
|
| buildTacletIndex | | public TacletIndex buildTacletIndex()(Code) | | Return a taclet index with no taclets in it.
|
| run | | public void run()(Code) | | Build an initial proof with a formula in it.
|
|
|