--- a/TFL/thry.sig Tue May 20 11:47:33 1997 +0200
+++ b/TFL/thry.sig Tue May 20 11:49:57 1997 +0200
@@ -1,30 +1,25 @@
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_term : theory -> term -> term
+ -> term binding list * typ binding list
- val match_type : Thry -> Type -> Type -> Type binding list
+ val match_type : theory -> typ -> typ -> typ binding list
- val typecheck : Thry -> Preterm -> Term
+ val typecheck : theory -> term -> cterm
- val make_definition: Thry -> string -> Preterm -> Thm * Thry
+ val make_definition: theory -> string -> term -> thm * theory
(* Datatype facts of various flavours *)
- val match_info: Thry -> string -> {constructors:Preterm list,
- case_const:Preterm} USyntax.Utils.option
+ val match_info: theory -> string -> {constructors:term list,
+ case_const:term} option
- val induct_info: Thry -> string -> {constructors:Preterm list,
- nchotomy:Thm} USyntax.Utils.option
+ val induct_info: theory -> string -> {constructors:term list,
+ nchotomy:thm} option
- val extract_info: Thry -> {case_congs:Thm list, case_rewrites:Thm list}
+ val extract_info: theory -> {case_congs:thm list, case_rewrites:thm list}
end;