changeset 9640 | 8c6cf4f01644 |
parent 8622 | 870a58dd0ddd |
child 9651 | f0cfddda6038 |
--- a/TFL/tfl.sig Thu Aug 17 18:30:48 2000 +0200 +++ b/TFL/tfl.sig Thu Aug 17 18:31:12 2000 +0200 @@ -13,7 +13,11 @@ val default_simps : thm list (*simprules used for deriving rules...*) - val congs : thm list -> thm list (*fn to make congruent rules*) + val Add_recdef_congs: thm list -> unit + val Del_recdef_congs: thm list -> unit + val init: theory -> theory + val print_recdef_congs: theory -> unit + val congs : theory -> thm list -> thm list (*fn to make congruence rules*) type pattern