src/proofman/proofManagerLib.sml

2 (* The programs here maintain a reference to an element of the proofs type.  *)
13 type proofs = Manager.proofs
20 fun proofs() = !the_proofs;
21 fun top_proof() = Manager.current_proof(proofs());
25    (the_proofs := Manager.add (Manager.new_goalstack g f) (proofs());
26     proofs());
29    (the_proofs := Manager.add (Manager.new_goaltree g) (proofs());
30     proofs());
39              the_proofs := Manager.add g (proofs());
40              proofs());
43    (the_proofs := Manager.hd_opr Manager.backup (proofs());
47    (the_proofs := Manager.hd_opr Manager.restore (proofs());
51    (the_proofs := Manager.hd_opr Manager.save (proofs());
57   (the_proofs := Manager.hd_opr (Manager.set_backup i) (proofs()));
60   (the_proofs := Manager.hd_opr (Manager.forget_history) (proofs()));
63    (the_proofs := Manager.hd_opr Manager.restart (proofs());
66 local fun primdrop() = (the_proofs := Manager.drop (proofs()));
68 fun drop() = (primdrop(); say"OK..\n"; proofs())
69         handle Manager.NO_PROOFS => proofs()
71    if i<1 then (say"OK..\n"; proofs()) else (primdrop(); dropn (i-1))
72    handle Manager.NO_PROOFS => proofs()
77     the_proofs := Manager.hd_opr (Manager.expandf tac) (proofs());
83     the_proofs := Manager.hd_opr (Manager.expand tac) (proofs());
89     the_proofs := Manager.hd_opr (Manager.expand_listf ltac) (proofs());
95     the_proofs := Manager.hd_opr (Manager.expand_list ltac) (proofs());
101     the_proofs := Manager.hd_opr (Manager.expandv (s,tac)) (proofs());
112 val top_thm      = Manager.hd_proj Manager.top_thm o proofs;
113 val initial_goal = Manager.hd_proj Manager.initial_goal o proofs;
114 val top_goal     = Manager.hd_proj Manager.top_goal o proofs;
115 val top_goals    = Manager.hd_proj Manager.top_goals o proofs;
117 fun p () = Manager.hd_proj I (proofs())
122 val status = proofs;
125   (the_proofs := Manager.hd_opr (Manager.flatn i) (proofs());
129   (the_proofs := Manager.hd_opr (Manager.rotate i) (proofs());
135    (the_proofs := Manager.rotate_proofs i (proofs());
136     proofs());