The first two subsections give a quick summary of proof and application of theorems which is useful in reading the previous section on the tactic langauge.

- Proving Theorems
- Applying Theorems as Rewrite Rules
- Features of the Proof Environment
- Starting Out
- Simple Permutations
- Term Display
- Local Term Manipulation
- Global Variable Assignment
- Finishing Up
- The Module System

Fri Sep 5 16:28:58 MDT 1997