author | wenzelm |
Tue, 18 Apr 2000 14:54:08 +0200 | |
changeset 8734 | b456aba346a6 |
parent 8733 | 3213613a775a |
child 8735 | bb2250ac9557 |
--- a/src/HOL/Tools/recdef_package.ML Tue Apr 18 00:49:49 2000 +0200 +++ b/src/HOL/Tools/recdef_package.ML Tue Apr 18 14:54:08 2000 +0200 @@ -163,7 +163,7 @@ OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl (defer_recdef_decl >> Toplevel.theory); -val _ = OuterSyntax.add_keywords ["congs", "simpset"]; +val _ = OuterSyntax.add_keywords ["congs"]; val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP]; end;