# HG changeset patch
# User haftmann
# Date 1324738389 -3600
# Node ID 03ce2b2a29a20a26473dcaef72b8ab3babd5a795
# Parent  2af982715e5c0f1fecb98daa0f5cdf907deff229
tuned proofs

diff -r 2af982715e5c -r 03ce2b2a29a2 src/HOL/Library/Reflection.thy
--- a/src/HOL/Library/Reflection.thy	Sat Dec 24 15:53:09 2011 +0100
+++ b/src/HOL/Library/Reflection.thy	Sat Dec 24 15:53:09 2011 +0100
@@ -12,7 +12,7 @@
 setup {* Reify_Data.setup *}
 
 lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
-  by (blast intro: ext)
+  by blast
 
 use "reflection.ML"
 
diff -r 2af982715e5c -r 03ce2b2a29a2 src/HOL/Nominal/Examples/Standardization.thy
--- a/src/HOL/Nominal/Examples/Standardization.thy	Sat Dec 24 15:53:09 2011 +0100
+++ b/src/HOL/Nominal/Examples/Standardization.thy	Sat Dec 24 15:53:09 2011 +0100
@@ -6,7 +6,7 @@
 header {* Standardization *}
 
 theory Standardization
-imports Nominal
+imports "../Nominal"
 begin
 
 text {*
@@ -426,11 +426,7 @@
 lemma listrelp_eqvt [eqvt]:
   assumes xy: "listrelp f (x::'a::pt_name list) y"
   shows "listrelp ((pi::name prm) \<bullet> f) (pi \<bullet> x) (pi \<bullet> y)" using xy
-  apply induct
-   apply (simp add: listrelp.intros)
-  apply simp
-  apply (metis listrelp.Cons in_eqvt mem_def perm_app pt_set_bij3)
-  done
+  by induct (simp_all add: listrelp.intros perm_app [symmetric])
 
 inductive
   sred :: "lam \<Rightarrow> lam \<Rightarrow> bool"  (infixl "\<rightarrow>\<^sub>s" 50)
diff -r 2af982715e5c -r 03ce2b2a29a2 src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Sat Dec 24 15:53:09 2011 +0100
+++ b/src/HOL/RComplete.thy	Sat Dec 24 15:53:09 2011 +0100
@@ -76,8 +76,7 @@
   from assms have "\<exists>X. X \<in> S" and "\<exists>Y. \<forall>x\<in>S. x \<le> Y"
     unfolding isUb_def setle_def by simp_all
   from complete_real [OF this] show ?thesis
-    unfolding isLub_def leastP_def setle_def setge_def Ball_def
-      Collect_def mem_def isUb_def UNIV_def by simp
+    by (simp add: isLub_def leastP_def isUb_def setle_def setge_def)
 qed
 
 
diff -r 2af982715e5c -r 03ce2b2a29a2 src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Sat Dec 24 15:53:09 2011 +0100
+++ b/src/HOL/SupInf.thy	Sat Dec 24 15:53:09 2011 +0100
@@ -356,7 +356,7 @@
 lemma Inf_greater:
   fixes z :: real
   shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
-  by (metis Inf_real_iff mem_def not_leE)
+  by (metis Inf_real_iff not_leE)
 
 lemma Inf_close:
   fixes e :: real
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). *}