Editing facilities are provided for proof-scripts, as are tactics for explicitly executing a proof-script on a node of a proof. These are particularly of use when fixing proof-scripts that have broken due to changes in tactics or the library context.
Proof scripts are Lisp data structures. They are made editable by translating to and from `proof-script terms' or `ps-terms' for short. An example display of a ps-term is:
Figure 
summarizes the structure of ps-terms.
The `alias' column gives the name by which proof-script nodes can be entered. Proof-script subtrees are considered to be a term sequence, and the usual term sequence editing commands work with them. The addr fields in ps-terms are for tree addresses in the same format as used in proofs. They serve solely as a guide the user; they have no logical significance. Users should never need to explicitly fill these addresses in. Instead, the addresses are generated by ML functions that build proof script terms.
Useful ML functions include:
psterm_of_thm_object nam:tok = psterm:term
psterm_anno psterm:term = psterm':term
RunPSTerm psterm:term = T:tactic
