changeset 55017 | 2df6ad1dbd66 |
parent 48891 | c0eafbd55de3 |
child 56248 | 67dc9549fa15 |
--- a/src/HOL/Library/Old_Recdef.thy Thu Jan 16 15:47:33 2014 +0100 +++ b/src/HOL/Library/Old_Recdef.thy Thu Jan 16 16:20:17 2014 +0100 @@ -5,7 +5,7 @@ header {* TFL: recursive function definitions *} theory Old_Recdef -imports Wfrec +imports Main keywords "recdef" "defer_recdef" :: thy_decl and "recdef_tc" :: thy_goal and