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