--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Fri Nov 03 21:33:15 2000 +0100
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Fri Nov 03 21:33:53 2000 +0100
@@ -223,7 +223,7 @@
also obtain i j where "?e a b = {(i, j)}"
proof -
have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
- thus ?thesis by blast
+ thus ?thesis by (blast intro: that)
qed
also have "... Un ?e t b = insert (i, j) (?e t b)" by simp
also have "card ... = Suc (card (?e t b))"
--- a/src/HOL/Isar_examples/W_correct.thy Fri Nov 03 21:33:15 2000 +0100
+++ b/src/HOL/Isar_examples/W_correct.thy Fri Nov 03 21:33:53 2000 +0100
@@ -119,7 +119,7 @@
and mgu_ok: "mgu ($ s2 t1) (t2 -> TVar n2) = Ok u"
and W1_ok: "W e1 a n = Ok (s1, t1, n1)"
and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)"
- by (auto split: bind_splits)
+ by (auto split: bind_splits simp: that)
show "$ s a |- App e1 e2 :: t"
proof (rule has_type.App)
from s have s': "$ u ($ s2 ($ s1 a)) = $s a"
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Fri Nov 03 21:33:15 2000 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Fri Nov 03 21:33:53 2000 +0100
@@ -307,7 +307,7 @@
with oX_Ref
obtain obj where
loc: "hp ref = Some obj" "obj_ty obj = RefT T'"
- by clarsimp
+ by auto
then
obtain D where
@@ -330,7 +330,7 @@
with mC' wfprog
obtain D0 rT0 maxl0 ins0 where
mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxl0, ins0)" "G\<turnstile>rT0\<preceq>rT"
- by (auto dest: subtype_widen_methd)
+ by (auto dest: subtype_widen_methd intro: that)
from X' D
have "G \<turnstile> D \<preceq>C X'"
@@ -340,7 +340,7 @@
obtain D'' rT' mxl' ins' where
mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxl', ins')"
"G \<turnstile> rT' \<preceq> rT0"
- by (auto dest: subtype_widen_methd)
+ by (auto dest: subtype_widen_methd intro: that)
from mX mD
have rT': "G \<turnstile> rT' \<preceq> rT"
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Fri Nov 03 21:33:15 2000 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Fri Nov 03 21:33:53 2000 +0100
@@ -138,7 +138,7 @@
\<and> graph F f \<subseteq> graph H h
\<and> (\<forall>x \<in> H. h x <= p x)"
by (simp! add: norm_pres_extension_D)
- thus ?thesis by (elim exE conjE) rule
+ with that show ?thesis by blast
qed
have h: "is_vectorspace H" ..
have "H = E"
@@ -157,7 +157,7 @@
have "H \<subseteq> E" ..
thus "H \<subset> E" ..
qed
- thus ?thesis by blast
+ with that show ?thesis by blast
qed
have x': "x' \<noteq> 0"
proof (rule classical)
@@ -194,7 +194,7 @@
thus "- p (u + x') - h u <= p (v + x') - h v"
by (rule real_diff_ineq_swap)
qed
- thus ?thesis by rule rule
+ thus ?thesis ..
qed
def h' == "\<lambda>x. let (y,a) = SOME (y,a). x = y + a \<cdot> x' \<and> y \<in> H