Up: LEGO System and Documentation, 1.3

New features in LEGO Version 1.3

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

LEGO maintainer
Last modified: Tue Jun 23 16:49:43 BST 1998