--- a/TFL/tfl.sig Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/tfl.sig Thu Jun 05 13:27:28 1997 +0200
@@ -15,23 +15,22 @@
-> {functional:term,
pats: pattern list}
- val wfrec_definition0 : theory -> string -> term -> term -> thm * theory
+ val wfrec_definition0 : theory -> string -> term -> term -> theory
- val post_definition : theory * (thm * pattern list)
- -> {theory : theory,
- rules : thm,
- TCs : term list list,
- full_pats_TCs : (term * term list) list,
- patterns : pattern list}
+ val post_definition : simpset -> theory * (thm * pattern list)
+ -> {theory : theory,
+ rules : thm,
+ TCs : term list list,
+ full_pats_TCs : (term * term list) list,
+ patterns : pattern list}
-
+(*CURRENTLY UNUSED
val wfrec_eqns : theory -> term list
-> {WFR : term,
proto_def : term,
extracta :(thm * term list) list,
pats : pattern list}
-
val lazyR_def : theory
-> term list
-> {theory:theory,
@@ -39,11 +38,9 @@
R :term,
full_pats_TCs :(term * term list) list,
patterns: pattern list}
+---------------------*)
- val mk_induction : theory
- -> term -> term
- -> (term * term list) list
- -> thm
+ val mk_induction : theory -> term -> term -> (term * term list) list -> thm
val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm}
-> theory