1signature Manager =
2sig
3 include Abbrev
4
5  datatype proof
6       = GOALSTACK of goalStack.gstk History.history
7       | GOALTREE of goalTree.gtree History.history
8
9  datatype proofs = PRFS of proof list
10  exception NO_PROOFS
11
12  (* Starting a proof *)
13  val new_goalstack  : goal -> (thm->thm) -> proof
14  val new_goaltree   : goal -> proof
15  val set_goal       : goal -> proof
16  val add            : proof -> proofs -> proofs
17
18  (* Undo *)
19  val backup         : proof -> proof
20  val set_backup     : int -> proof -> proof
21  val restore        : proof -> proof
22  val save           : proof -> proof
23  val forget_history : proof -> proof
24  val restart        : proof -> proof
25  val drop           : proofs -> proofs
26
27  (* Applying a tactic to a goal *)
28  val expand         : tactic -> proof -> proof
29  val expandf        : tactic -> proof -> proof
30  val expand_list    : list_tactic -> proof -> proof
31  val expand_listf   : list_tactic -> proof -> proof
32  val expandv        : string * tactic -> proof -> proof
33
34  (* Seeing what the state of the proof manager is *)
35  val top_thm        : proof -> thm
36  val initial_goal   : proof -> goal
37  val finalizer      : proof -> (thm -> thm)
38  val top_goal       : proof -> goal
39  val top_goals      : proof -> goal list
40  val current_proof  : proofs -> proof
41
42  (* Switch focus to a different subgoal (or proof attempt) *)
43  val rotate         : int -> proof -> proof
44  val flatn          : int -> proof -> proof
45  val rotate_proofs  : int -> proofs -> proofs
46
47  (* Operations on proof attempts *)
48  val hd_opr         : (proof -> proof) -> proofs -> proofs
49  val hd_proj        : (proof -> 'a) -> proofs -> 'a
50
51  val initial_proofs : unit -> proofs
52  val set_goal_pp    : goal Parse.pprinter -> goal Parse.pprinter
53  val std_goal_pp    : goal Parse.pprinter
54
55  val pp_proof       : proof Parse.pprinter
56  val pp_proofs      : proofs Parse.pprinter
57
58end
59