1signature goalStack = 2sig 3 include Abbrev 4 5 type gstk 6 7 val chatting : bool ref 8 9 val expand : tactic -> gstk -> gstk 10 val expandf : tactic -> gstk -> gstk 11 val expand_list : list_tactic -> gstk -> gstk 12 val expand_listf : list_tactic -> gstk -> gstk 13 val print_tac : string -> tactic 14 val extract_thm : gstk -> thm 15 val initial_goal : gstk -> goal 16 val finalizer : gstk -> thm -> thm 17 val is_initial : gstk -> bool 18 val new_goal : goal -> (thm -> thm) -> gstk 19 val rotate : gstk -> int -> gstk 20 val flatn : gstk -> int -> gstk 21 val top_goal : gstk -> goal 22 val top_goals : gstk -> goal list 23 val depth : gstk -> int 24 val goal_size : goal -> int 25 val gstk_size : gstk -> int 26 27 val std_pp_goal : goal Parse.pprinter 28 val pp_goal : goal Parse.pprinter 29 val pp_gstk : gstk Parse.pprinter 30 val set_goal_pp : goal Parse.pprinter -> goal Parse.pprinter 31 32end 33