1signature Conversion = 2sig 3 4 include Abbrev 5 6 val base_defn_list : thm list 7 8 val CONV : conv 9 10 val STE_CONV_RULE : thm -> thm list -> thm 11 12 val add_next : int -> term -> term 13 val add_next_upto_depth : int -> int -> term -> term 14 15 val TrajForm : term * string * term * int * int -> term 16 val TF : (term * string * term * int * int) list -> term 17 18 val extract_constr : thm -> term 19 20 val STE : term -> term -> term -> thm list -> bool -> thm 21 22 val STE_TO_BOOL : term -> term -> term -> term -> thm -> thm -> thm -> thm 23 24end (* sig *) 25