author | wenzelm |
Fri, 15 Sep 2000 20:22:36 +0200 | |
changeset 9999 | 566c6b906370 |
parent 9998 | 09bf8fcd1c6e |
child 10000 | fe6ffa46266f |
--- a/src/HOL/Tools/recdef_package.ML Fri Sep 15 20:22:00 2000 +0200 +++ b/src/HOL/Tools/recdef_package.ML Fri Sep 15 20:22:36 2000 +0200 @@ -329,7 +329,7 @@ OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl (defer_recdef_decl >> Toplevel.theory); -val _ = OuterSyntax.add_keywords ["hints"]; +val _ = OuterSyntax.add_keywords ["congs", "hints"]; val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP]; end;