1.1 --- a/src/HOL/Set.thy	Tue Jul 12 11:55:33 2005 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Jul 12 12:49:00 2005 +0200
     1.3 @@ -1110,10 +1110,10 @@
     1.4  text {* \medskip Monotonicity. *}
     1.5  
     1.6  lemma mono_Un: "mono f ==> f A \<union> f B \<subseteq> f (A \<union> B)"
     1.7 -  by (blast dest: monoD)
     1.8 +  by (auto simp add: mono_def)
     1.9  
    1.10  lemma mono_Int: "mono f ==> f (A \<inter> B) \<subseteq> f A \<inter> f B"
    1.11 -  by (blast dest: monoD)
    1.12 +  by (auto simp add: mono_def)
    1.13  
    1.14  subsubsection {* Equalities involving union, intersection, inclusion, etc. *}
    1.15  
    1.16 @@ -1199,12 +1199,12 @@
    1.17  lemma insert_disjoint[simp]:
    1.18   "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
    1.19   "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"
    1.20 -by auto
    1.21 +  by auto
    1.22  
    1.23  lemma disjoint_insert[simp]:
    1.24   "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
    1.25   "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
    1.26 -by auto
    1.27 +  by auto
    1.28  
    1.29  text {* \medskip @{text image}. *}
    1.30  
    1.31 @@ -1215,7 +1215,7 @@
    1.32    by blast
    1.33  
    1.34  lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
    1.35 -  by blast
    1.36 +  by auto
    1.37  
    1.38  lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
    1.39    by blast
    1.40 @@ -1226,10 +1226,11 @@
    1.41  lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
    1.42    by blast
    1.43  
    1.44 +
    1.45  lemma image_Collect: "f ` {x. P x} = {f x | x. P x}"
    1.46 -  -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS, *}
    1.47 -  -- {* with its implicit quantifier and conjunction.  Also image enjoys better *}
    1.48 -  -- {* equational properties than does the RHS. *}
    1.49 +  -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
    1.50 +      with its implicit quantifier and conjunction.  Also image enjoys better
    1.51 +      equational properties than does the RHS. *}
    1.52    by blast
    1.53  
    1.54  lemma if_image_distrib [simp]: