10SN/Asignature Manager = 20SN/Asig 316772Slana include Abbrev 40SN/A 50SN/A datatype proof 60SN/A = GOALSTACK of goalStack.gstk History.history 70SN/A | GOALTREE of goalTree.gtree History.history 82362SN/A 90SN/A datatype proofs = PRFS of proof list 102362SN/A exception NO_PROOFS 110SN/A 120SN/A (* Starting a proof *) 130SN/A val new_goalstack : goal -> (thm->thm) -> proof 140SN/A val new_goaltree : goal -> proof 150SN/A val set_goal : goal -> proof 160SN/A val add : proof -> proofs -> proofs 170SN/A 180SN/A (* Undo *) 190SN/A val backup : proof -> proof 200SN/A val set_backup : int -> proof -> proof 210SN/A val restore : proof -> proof 222362SN/A val save : proof -> proof 232362SN/A val forget_history : proof -> proof 242362SN/A val restart : proof -> proof 250SN/A val drop : proofs -> proofs 260SN/A 270SN/A (* Applying a tactic to a goal *) 283516SN/A val expand : tactic -> proof -> proof 290SN/A val expandf : tactic -> proof -> proof 300SN/A val expand_list : list_tactic -> proof -> proof 313516SN/A val expand_listf : list_tactic -> proof -> proof 320SN/A val expandv : string * tactic -> proof -> proof 330SN/A 343516SN/A (* Seeing what the state of the proof manager is *) 350SN/A val top_thm : proof -> thm 360SN/A val initial_goal : proof -> goal 373516SN/A val finalizer : proof -> (thm -> thm) 380SN/A val top_goal : proof -> goal 390SN/A val top_goals : proof -> goal list 403516SN/A val current_proof : proofs -> proof 410SN/A 420SN/A (* Switch focus to a different subgoal (or proof attempt) *) 433516SN/A val rotate : int -> proof -> proof 440SN/A val flatn : int -> proof -> proof 450SN/A val rotate_proofs : int -> proofs -> proofs 463516SN/A 470SN/A (* Operations on proof attempts *) 480SN/A val hd_opr : (proof -> proof) -> proofs -> proofs 490SN/A val hd_proj : (proof -> 'a) -> proofs -> 'a 503516SN/A 510SN/A val initial_proofs : unit -> proofs 520SN/A val set_goal_pp : goal Parse.pprinter -> goal Parse.pprinter 530SN/A val std_goal_pp : goal Parse.pprinter 543516SN/A 550SN/A val pp_proof : proof Parse.pprinter 560SN/A val pp_proofs : proofs Parse.pprinter 573516SN/A 583516SN/Aend 593516SN/A