src/HOL/Library/Old_Recdef.thy
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