--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/thry.sig Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,31 @@
+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;
+
+