summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 03 Nov 2000 21:33:53 +0100 | |

changeset 10387 | 9dac2cad5500 |

parent 10386 | 581a5a143994 |

child 10388 | ac1ae85a5605 |

adapted "obtain" proofs;

--- 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