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