Structural

Id

The identity tactic.

A tactic which always fails. Usually used inside other tactics.

Proves goals of form where A is the ith hypothesis.

Proves goals of form or or where is the ith declaration.

Assert term t before hypothesis j. Generates main subgoal with t asserted, and assertion subgoal to prove t.

AssertAt 0 t. Assert t as last hypothesis.

Move hyp j to before hyp i.

If hyp j is a proposition,  



If hyp j is a declaration,



MoveToConcl first invokes itself recursively on any hyp which might depend on hyp j.

MoveDepHypsToConcl j

Use MoveToConcl to move hyps which use variable declared by hyp j. 

Thin i

Delete hypothesis i. 

RenameVar v i

Rename the variable declared in hypothesis i to v. 

RenameBVars (vsub : (var # var) list) c

Rename occurrences of bound variables in clause c.