| 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 |