The Proof Environment

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
  • Declaring Pretheorems
• 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