1signature psMinimize =
2sig
3
4  include Abbrev
5
6  datatype Proof =
7    Tactic of (string * goal)
8  | Then   of (Proof * Proof)
9  | Thenl  of (Proof * Proof list)
10
11  val mini_tactic_time : real ref
12  val mini_proof_time : real ref
13
14  val minimize_stac : real -> string -> goal -> goal list -> string
15  val requote_sproof : string -> string
16  val minimize_proof : Proof -> Proof
17  val reconstruct : goal -> Proof -> string
18
19end
20