changeset 60523 | be2d9f5ddc76 |
parent 60520 | 09fc5eaa21ce |
child 67091 | 1393c2340eec |
--- a/src/HOL/Library/Old_Recdef.thy Fri Jun 19 19:45:01 2015 +0200 +++ b/src/HOL/Library/Old_Recdef.thy Fri Jun 19 20:14:50 2015 +0200 @@ -7,8 +7,7 @@ theory Old_Recdef imports Main keywords - "recdef" "defer_recdef" :: thy_decl and - "recdef_tc" :: thy_goal and + "recdef" :: thy_decl and "permissive" "congs" "hints" begin