diff -r d64d48eb71cc -r 4af607652318 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Feb 10 16:09:30 2015 +0000
+++ b/src/HOL/Set.thy	Tue Feb 10 17:37:06 2015 +0000
@@ -1058,7 +1058,7 @@
   "{u. \<exists>x. u = f x} = range f"
   by auto
 
-lemma range_composition: 
+lemma range_composition:
   "range (\<lambda>x. f (g x)) = f ` range g"
   by auto
 
@@ -1244,7 +1244,7 @@
 lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \<inter> {x. Q x}"
   by blast
 
-lemma Collect_mono_iff [simp]: "Collect P \<subseteq> Collect Q \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q x)"
+lemma Collect_mono_iff: "Collect P \<subseteq> Collect Q \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q x)"
   by blast
 
 
@@ -1809,7 +1809,7 @@
 by blast
 
 lemma image_subset_iff_subset_vimage: "f ` A \<subseteq> B \<longleftrightarrow> A \<subseteq> f -` B"
-  by blast 
+  by blast
 
 lemma vimage_const [simp]: "((\<lambda>x. c) -` A) = (if c \<in> A then UNIV else {})"
   by auto