changeset 9651 | f0cfddda6038 |
parent 9640 | 8c6cf4f01644 |
--- a/TFL/tfl.sig Fri Aug 18 17:53:49 2000 +0200 +++ b/TFL/tfl.sig Fri Aug 18 17:58:33 2000 +0200 @@ -25,7 +25,7 @@ -> {functional:term, pats: pattern list} - val wfrec_definition0 : theory -> string -> term -> term -> theory + val wfrec_definition0 : theory -> string -> term -> term -> theory * thm val post_definition : thm list -> theory * (thm * pattern list) -> {theory : theory,