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)"