changeset 46950 | d0181abdbdac |
parent 46947 | b8c7eb0c2f89 |
child 48891 | c0eafbd55de3 |
--- a/src/HOL/Library/Old_Recdef.thy Thu Mar 15 20:07:00 2012 +0100 +++ b/src/HOL/Library/Old_Recdef.thy Thu Mar 15 22:08:53 2012 +0100 @@ -6,7 +6,10 @@ theory Old_Recdef imports Wfrec -keywords "recdef" :: thy_decl and "permissive" "congs" "hints" +keywords + "recdef" "defer_recdef" :: thy_decl and + "recdef_tc" :: thy_goal and + "permissive" "congs" "hints" uses ("~~/src/HOL/Tools/TFL/casesplit.ML") ("~~/src/HOL/Tools/TFL/utils.ML")