--- a/TFL/tfl.sig Thu May 15 11:35:26 1997 +0200
+++ b/TFL/tfl.sig Thu May 15 12:29:59 1997 +0200
@@ -18,9 +18,15 @@
-> {functional:Preterm,
pats: pattern list}
- val prim_wfrec_definition : Thry
- -> {R:Preterm, functional:Preterm}
- -> {def:Thm, corollary:Thm, theory:Thry}
+ val wfrec_definition0 : Thry -> Preterm -> Preterm -> Thm * Thry
+
+ val post_definition : Thry * (Thm * pattern list)
+ -> {theory : Thry,
+ rules : Thm,
+ TCs : Preterm list list,
+ full_pats_TCs : (Preterm * Preterm list) list,
+ patterns : pattern list}
+
val wfrec_eqns : Thry -> Preterm
-> {WFR : Preterm,
@@ -29,14 +35,6 @@
pats : pattern list}
- val gen_wfrec_definition : Thry
- -> {R:Preterm, eqs:Preterm}
- -> {theory:Thry,
- rules :Thm,
- TCs : Preterm list list,
- full_pats_TCs :(Preterm * Preterm list) list,
- patterns : pattern list}
-
val lazyR_def : Thry
-> Preterm
-> {theory:Thry,
@@ -55,8 +53,6 @@
-> {rules:Thm, induction:Thm, TCs:Preterm list list}
-> {rules:Thm, induction:Thm, nested_tcs:Thm list}
- val termination_goals : Thm -> Preterm list
-
structure Context
: sig
val read : unit -> Thm list