# Structure Manager

signature Manager =
sig
include Abbrev
datatype proof
= GOALSTACK of goalStack.gstk History.history
| GOALTREE of goalTree.gtree History.history
datatype proofs = PRFS of proof list
exception NO_PROOFS
(* Starting a proof *)
val new_goalstack : goal -> (thm->thm) -> proof
val new_goaltree : goal -> proof
val set_goal : goal -> proof
val add : proof -> proofs -> proofs
(* Undo *)
val backup : proof -> proof
val set_backup : int -> proof -> proof
val restore : proof -> proof
val save : proof -> proof
val forget_history : proof -> proof
val restart : proof -> proof
val drop : proofs -> proofs
(* Applying a tactic to a goal *)
val expand : tactic -> proof -> proof
val expandf : tactic -> proof -> proof
val expand_list : list_tactic -> proof -> proof
val expand_listf : list_tactic -> proof -> proof
val expandv : string * tactic -> proof -> proof
(* Seeing what the state of the proof manager is *)
val top_thm : proof -> thm
val initial_goal : proof -> goal
val finalizer : proof -> (thm -> thm)
val top_goal : proof -> goal
val top_goals : proof -> goal list
val current_proof : proofs -> proof
(* Switch focus to a different subgoal (or proof attempt) *)
val rotate : int -> proof -> proof
val flatn : int -> proof -> proof
val rotate_proofs : int -> proofs -> proofs
(* Operations on proof attempts *)
val hd_opr : (proof -> proof) -> proofs -> proofs
val hd_proj : (proof -> 'a) -> proofs -> 'a
val initial_proofs : unit -> proofs
val set_goal_pp : goal Parse.pprinter -> goal Parse.pprinter
val std_goal_pp : goal Parse.pprinter
val pp_proof : proof Parse.pprinter
val pp_proofs : proofs Parse.pprinter
end

*HOL 4, Kananaskis-13*