TFL/thry.sig

+signature Thry_sig =
+sig
+  type Type
+  type Preterm
+  type Term
+  type Thm
+  type Thry
+  type 'a binding
+
+  structure USyntax : USyntax_sig
+  val match_term : Thry -> Preterm -> Preterm 
+                    -> Preterm binding list * Type binding list
+
+  val match_type : Thry -> Type -> Type -> Type binding list
+
+  val typecheck : Thry -> Preterm -> Term
+
+  val make_definition: Thry -> string -> Preterm -> Thm * Thry
+
+  (* Datatype facts of various flavours *)
+  val match_info: Thry -> string -> {constructors:Preterm list,
+                                     case_const:Preterm} USyntax.Utils.option
+
+  val induct_info: Thry -> string -> {constructors:Preterm list,
+                                      nchotomy:Thm} USyntax.Utils.option
+
+  val extract_info: Thry -> {case_congs:Thm list, case_rewrites:Thm list}
+
+end;
+
+