Assumption Tactic | a cut-down version of the Immed tactic |
Configure Equality | sets up the equality to be used by various commands |
Elimination Rule for Relations | hypotheses of inductive clauses are now directly accessible |
Induction | induction tactic |
Infix Notation | a syntactic class of infix operators |
Inversion and Invert | inverting the derivation of an inductively defined relation |
qnify, Qnify and Configure Qnify | support for first-order unification problems |
Relaxed Patterns and Inductive Types | functional abstraction on the right-hand side of reduction rules |
Speedups | towards a lazy functional programming language |
Then | almost a THEN tactical in the LCF spirit |
Theorems and Configure Theorems | a suite of theorems for inductive datatypes for free |
UTac | integrate tactics written in ML |