# HG changeset patch
# User paulson
# Date 1121165340 -7200
# Node ID 33c4d8fe6f78af04538e884c0575f731823e33fc
# Parent  fe9dfbc2fa3fd8db84a2356231c165833a51efb1
tweaked

diff -r fe9dfbc2fa3f -r 33c4d8fe6f78 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Jul 12 11:55:33 2005 +0200
+++ b/src/HOL/Set.thy	Tue Jul 12 12:49:00 2005 +0200
@@ -1110,10 +1110,10 @@
 text {* \medskip Monotonicity. *}
 
 lemma mono_Un: "mono f ==> f A \<union> f B \<subseteq> f (A \<union> B)"
-  by (blast dest: monoD)
+  by (auto simp add: mono_def)
 
 lemma mono_Int: "mono f ==> f (A \<inter> B) \<subseteq> f A \<inter> f B"
-  by (blast dest: monoD)
+  by (auto simp add: mono_def)
 
 subsubsection {* Equalities involving union, intersection, inclusion, etc. *}
 
@@ -1199,12 +1199,12 @@
 lemma insert_disjoint[simp]:
  "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
  "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"
-by auto
+  by auto
 
 lemma disjoint_insert[simp]:
  "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
  "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
-by auto
+  by auto
 
 text {* \medskip @{text image}. *}
 
@@ -1215,7 +1215,7 @@
   by blast
 
 lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
-  by blast
+  by auto
 
 lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
   by blast
@@ -1226,10 +1226,11 @@
 lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
   by blast
 
+
 lemma image_Collect: "f ` {x. P x} = {f x | x. P x}"
-  -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS, *}
-  -- {* with its implicit quantifier and conjunction.  Also image enjoys better *}
-  -- {* equational properties than does the RHS. *}
+  -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
+      with its implicit quantifier and conjunction.  Also image enjoys better
+      equational properties than does the RHS. *}
   by blast
 
 lemma if_image_distrib [simp]: