--- 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"
--- 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)
--- 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
--- 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
--- 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). *}