author | wenzelm |
Fri, 15 Sep 2000 19:34:28 +0200 | |
changeset 9991 | fdead18501ca |
parent 9990 | 09c65992894c |
child 9992 | 4281ccea43f0 |
--- a/src/HOL/Tools/recdef_package.ML Fri Sep 15 19:32:27 2000 +0200 +++ b/src/HOL/Tools/recdef_package.ML Fri Sep 15 19:34:28 2000 +0200 @@ -329,6 +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_parsers [recdefP, defer_recdefP]; end;