src/HOL/BNF_Def.thy
changeset 55085 0e8e4dc55866
parent 55066 4e5ddf3162ac
child 55163 a740f312d9e4
     1.1 --- a/src/HOL/BNF_Def.thy	Mon Jan 20 20:42:43 2014 +0100
     1.2 +++ b/src/HOL/BNF_Def.thy	Mon Jan 20 21:32:41 2014 +0100
     1.3 @@ -8,9 +8,7 @@
     1.4  header {* Definition of Bounded Natural Functors *}
     1.5  
     1.6  theory BNF_Def
     1.7 -imports BNF_Util
     1.8 -   (*FIXME: register fundef_cong attribute in an interpretation to remove this dependency*)
     1.9 -  FunDef
    1.10 +imports BNF_Util Fun_Def_Base
    1.11  keywords
    1.12    "print_bnfs" :: diag and
    1.13    "bnf" :: thy_goal