TFL/tfl.sig
changeset 3191 14bd6e5985f1
parent 2112 3902e9af752f
child 3245 241838c01caf
--- 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