src/HOL/Codatatype/Basic_BNFs.thy
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]