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