diff -r 2af982715e5c -r 03ce2b2a29a2 src/HOL/ex/Set_Theory.thy
--- a/src/HOL/ex/Set_Theory.thy	Sat Dec 24 15:53:09 2011 +0100
+++ b/src/HOL/ex/Set_Theory.thy	Sat Dec 24 15:53:09 2011 +0100
@@ -179,7 +179,7 @@
 
 lemma "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>A. a \<notin> A \<and> b \<in> A \<and> c \<notin> A"
   -- {* Example 4. *}
-  by force
+  by auto --{*slow*}
 
 lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
   -- {*Example 5, page 298. *}
@@ -194,9 +194,9 @@
   by force
 
 lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
-    \<longrightarrow> (\<exists>A::int set. (\<forall>y. abs y \<notin> A) \<and> -2 \<in> A)"
-  -- {* Example 8 now needs a small hint. *}
-  by (simp add: abs_if, force)
+    \<longrightarrow> (\<exists>A::int set. -2 \<in> A & (\<forall>y. abs y \<notin> A))"
+  -- {* Example 8 needs a small hint. *}
+  by force
     -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *}
 
 text {* Example 9 omitted (requires the reals). *}