changeset 49310 | 6e30078de4f0 |
parent 49309 | f20b24214ac2 |
child 49312 | c874ff5658dc |
--- a/src/HOL/Codatatype/Basic_BNFs.thy Wed Sep 12 05:21:47 2012 +0200 +++ b/src/HOL/Codatatype/Basic_BNFs.thy Wed Sep 12 05:29:21 2012 +0200 @@ -10,7 +10,7 @@ header {* Registration of Basic Types as Bounded Natural Functors *} theory Basic_BNFs -imports BNF_Def "~~/src/HOL/Quotient_Examples/FSet" "~~/src/HOL/Library/Multiset" Countable_Set +imports BNF_Def begin lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]