src/HOL/Codatatype/BNF_Util.thy
changeset 49313 3f8671b353ae
parent 49312 c874ff5658dc
child 49314 f252c7c2ac7b
--- a/src/HOL/Codatatype/BNF_Util.thy	Wed Sep 12 06:27:48 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Util.thy	Wed Sep 12 06:30:35 2012 +0200
@@ -12,7 +12,6 @@
 imports
   "../Cardinals/Cardinal_Arithmetic"
   "~~/src/HOL/Library/Prefix_Order"
-  Equiv_Relations_More
 begin
 
 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"