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