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