1signature proofManagerLib =
2sig
3    include Abbrev
4    type proof = Manager.proof
5    type proofs = Manager.proofs
6
7    val chatting : bool ref
8
9    (* Starting a proof *)
10
11    val g             : term quotation -> proofs
12    val gt            : term quotation -> proofs
13    val set_goal      : goal -> proofs
14    val set_goaltree  : goal -> proofs
15    val new_goalstack : goal -> (thm -> thm) -> proofs
16    val new_goaltree  : goal -> proofs
17    val add           : proof -> proofs
18
19    (* Undo *)
20
21    val b             : unit -> proof
22    val drop          : unit -> proofs
23    val dropn         : int -> proofs
24    val drop_all      : unit -> proofs
25    val restart       : unit -> proof
26    val backup        : unit -> proof
27    val restore       : unit -> proof
28    val save          : unit -> proof
29    val set_backup    : int -> unit
30    val forget_history: unit -> unit
31
32    (* Applying a tactic to the current goal *)
33
34    val e             : tactic -> proof
35    val elt           : list_tactic -> proof
36    val eall          : tactic -> proof
37    val eta           : tactic -> proof
38    val enth          : tactic -> int -> proof
39    val et            : string * tactic -> proof
40    val expand        : tactic -> proof
41    val expandf       : tactic -> proof
42    val expand_list   : list_tactic -> proof
43    val expand_listf  : list_tactic -> proof
44    val expandv       : string * tactic -> proof
45
46    (* Seeing what the state of the proof manager is *)
47
48    val p             : unit -> proof
49    val initial_goal  : unit -> goal
50    val top_thm       : unit -> thm
51    val top_goal      : unit -> goal
52    val top_goals     : unit -> goal list
53    val status        : unit -> proofs
54
55    (* Switch focus to a different subgoal (or proof attempt) *)
56
57    val r             : int -> proof
58    val R             : int -> proofs
59    val rotate        : int -> proof
60    val flatn         : int -> proof
61    val rotate_proofs : int -> proofs
62
63    (* Switch to a different prettyprinter for all goals *)
64
65    val set_goal_pp   : goal Parse.pprinter -> goal Parse.pprinter
66
67    (* Standard system prettyprinter for goals *)
68
69    val std_goal_pp   : goal Parse.pprinter
70
71    (* Prettyprinters for the state of the proof manager *)
72
73    val pp_proof      : proof Parse.pprinter
74    val pp_proofs     : proofs Parse.pprinter
75end
76