The mechanism the system uses for certifying proof legitimacy is mediated by THM objects. THM objects are marked as complete and correct, partial and correct, or bad.

Bad THMs are those in which some tactic fails or the goal has free variables.

Partial THMs have correct steps, but have subgoals that have not been proved.

References to THM objects having the form "Thm* i:. i0" will include the "*" character to indicate that the THM object is good and complete.

To Store a Proof to a THM object, one first connects the THM object with the proof term with the following operator

Proof of fubar Ob Not Found: fubar

<pf term>

where the name of the THM object, say fubar, is in the string slot and the proof term goes in the term slot. The content of the THM object, if there is any, will be shown but not editable, and will display as ?fubar?.

To store the proof to the THM object, locate the point on the Proof-of operator and execute `(c-a)(c-v)' (which is the generic command for posting data to objects indirectly, which is to say, to objects other than the one being edited).

When a THM object is viewed or created, this Proof-of operator is automatically created for you. The PF menu accessible from MainMenu also contains a button for inserting it.

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html