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