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