author wenzelm Fri, 03 Nov 2000 21:33:53 +0100 changeset 10387 9dac2cad5500 parent 10386 581a5a143994 child 10388 ac1ae85a5605
```--- 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```