# HG changeset patch
# User wenzelm
# Date 973283633 -3600
# Node ID 9dac2cad550097d381c7572ae69fcb0c9a3d7edc
# Parent  581a5a143994a1c31aea9501d1a6a3205f1ec81d
adapted "obtain" proofs;

diff -r 581a5a143994 -r 9dac2cad5500 src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- 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))"
diff -r 581a5a143994 -r 9dac2cad5500 src/HOL/Isar_examples/W_correct.thy
--- 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"
diff -r 581a5a143994 -r 9dac2cad5500 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- 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"
diff -r 581a5a143994 -r 9dac2cad5500 src/HOL/Real/HahnBanach/HahnBanach.thy
--- 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