next up previous contents
Next: Applying Theorems as Rewrite Up: Proving Theorems Previous: Proving Theorems

Declaring Pretheorems

It is necessary when ``proving'' recursive or mutually recursive tactics to introduce embedded instances of theorems which have not yet been proved. The rule infix introduction commands do check for existence of theorems, so it is necessary to use the declarepretheorem command to signal the future intention of proving a theorem with the recursively introduced name.

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997