# HG changeset patch
# User wenzelm
# Date 1181752211 -7200
# Node ID ead82c82da9e9343e409c2af7dda50a79d9374be
# Parent  0035be079bee2da7daacc2eae2364590cc7ef533
tuned proofs: avoid implicit prems;

diff -r 0035be079bee -r ead82c82da9e src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -2680,8 +2680,8 @@
     qed
   next
     case (Super s L accC T A)
-    have conf_s: "Norm s\<Colon>\<preceq>(G, L)" .
-    have     wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T" .
+    note conf_s = `Norm s\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T`
     then obtain C c where
              C: "L This = Some (Class C)" and
        neq_Obj: "C\<noteq>Object" and
@@ -3426,10 +3426,10 @@
       have "\<And> j. abrupt s2 = Some (Jump j) \<Longrightarrow> j=Ret"
 	by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp)
       moreover 
-      have "s3 =
+      note `s3 =
                 (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> 
                         abrupt s2 = Some (Jump (Cont l))
-                 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)" .
+                 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)`
       ultimately show ?thesis
 	by force
     qed
@@ -3649,8 +3649,8 @@
 	from eval_e1 wt_e1 da_e1 wf True
 	have "nrm E1 \<subseteq> dom (locals (store s1))"
 	  by (cases rule: da_good_approxE') iprover
-	with da_e2 show ?thesis
-	  by (rule da_weakenE)
+	with da_e2 show thesis
+	  by (rule da_weakenE) (rule that)
       qed
       with conf_s1 wt_e2
       obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
diff -r 0035be079bee -r ead82c82da9e src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Extraction/Higman.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -146,16 +146,18 @@
   assumes ab: "a \<noteq> b" and bar: "bar xs"
   shows "\<And>ys zs. bar ys \<Longrightarrow> T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" using bar
 proof induct
-  fix xs zs assume "good xs" and "T a xs zs"
-  show "bar zs" by (rule bar1) (rule lemma3)
+  fix xs zs assume "T a xs zs" and "good xs"
+  hence "good zs" by (rule lemma3)
+  then show "bar zs" by (rule bar1)
 next
   fix xs ys
   assume I: "\<And>w ys zs. bar ys \<Longrightarrow> T a (w # xs) zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
   assume "bar ys"
   thus "\<And>zs. T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
   proof induct
-    fix ys zs assume "good ys" and "T b ys zs"
-    show "bar zs" by (rule bar1) (rule lemma3)
+    fix ys zs assume "T b ys zs" and "good ys"
+    then have "good zs" by (rule lemma3)
+    then show "bar zs" by (rule bar1)
   next
     fix ys zs assume I': "\<And>w zs. T a xs zs \<Longrightarrow> T b (w # ys) zs \<Longrightarrow> bar zs"
     and ys: "\<And>w. bar (w # ys)" and Ta: "T a xs zs" and Tb: "T b ys zs"
@@ -189,8 +191,9 @@
   shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> R a xs zs \<Longrightarrow> bar zs" using bar
 proof induct
   fix xs zs
-  assume "good xs" and "R a xs zs"
-  show "bar zs" by (rule bar1) (rule lemma2)
+  assume "R a xs zs" and "good xs"
+  then have "good zs" by (rule lemma2)
+  then show "bar zs" by (rule bar1)
 next
   fix xs zs
   assume I: "\<And>w zs. w # xs \<noteq> [] \<Longrightarrow> R a (w # xs) zs \<Longrightarrow> bar zs"
@@ -299,7 +302,7 @@
   thus ?case by iprover
 next
   case (bar2 ws)
-  have "is_prefix (f (length ws) # ws) f" by simp
+  from bar2.prems have "is_prefix (f (length ws) # ws) f" by simp
   thus ?case by (iprover intro: bar2)
 qed
 
diff -r 0035be079bee -r ead82c82da9e src/HOL/Extraction/QuotRem.thy
--- a/src/HOL/Extraction/QuotRem.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Extraction/QuotRem.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -30,7 +30,7 @@
     thus ?case by iprover
   next
     assume "r \<noteq> b"
-    hence "r < b" by (simp add: order_less_le)
+    with `r \<le> b` have "r < b" by (simp add: order_less_le)
     with I have "Suc a = Suc b * q + (Suc r) \<and> (Suc r) \<le> b" by simp
     thus ?case by iprover
   qed
diff -r 0035be079bee -r ead82c82da9e src/HOL/Extraction/Warshall.thy
--- a/src/HOL/Extraction/Warshall.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Extraction/Warshall.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -111,9 +111,10 @@
    (\<exists>q. is_path r q i j i) \<and> (\<exists>q'. is_path r q' i i k)"
 proof (simp cong add: conj_cong add: split_paired_all is_path_def, (erule conjE)+)
   fix xs
-  assume "list_all (\<lambda>x. x < Suc i) xs"
-  assume "is_path' r j xs k"
-  assume "\<not> list_all (\<lambda>x. x < i) xs"
+  assume asms:
+    "list_all (\<lambda>x. x < Suc i) xs"
+    "is_path' r j xs k"
+    "\<not> list_all (\<lambda>x. x < i) xs"
   show "(\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r j ys i) \<and>
     (\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys k)"
   proof
@@ -182,7 +183,7 @@
       	qed
       qed
     qed
-  qed
+  qed (rule asms)+
 qed
 
 theorem lemma5':
diff -r 0035be079bee -r ead82c82da9e src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Transition.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/IMP/Transition.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -366,7 +366,7 @@
   "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
 proof
   assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
-  show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1)
+  then show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1)
 next
   assume "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
   then obtain n where "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
@@ -460,7 +460,7 @@
 proof -
   assume "\<not>b s"
   have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
-  also have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" ..
+  also from `\<not>b s` have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" ..
   also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" ..
   finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
 qed
@@ -471,7 +471,7 @@
 proof -
   assume "b s"
   have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
-  also have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c;?w, s\<rangle>" ..
+  also from `b s` have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c;?w, s\<rangle>" ..
   finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>" ..
 qed
 
diff -r 0035be079bee -r ead82c82da9e src/HOL/Isar_examples/BasicLogic.thy
--- a/src/HOL/Isar_examples/BasicLogic.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -45,8 +45,8 @@
       assume A
       show C
       proof (rule mp)
-        show "B --> C" by (rule mp)
-        show B by (rule mp)
+        show "B --> C" by (rule mp) assumption+
+        show B by (rule mp) assumption+
       qed
     qed
   qed
@@ -65,7 +65,7 @@
 lemma "A --> A"
 proof
   assume A
-  show A .
+  show A by assumption
 qed
 
 text {*
@@ -117,7 +117,7 @@
 lemma "A --> B --> A"
 proof (intro impI)
   assume A
-  show A .
+  show A by assumption
 qed
 
 text {*
@@ -162,8 +162,8 @@
   assume "A & B"
   show "B & A"
   proof
-    show B by (rule conjunct2)
-    show A by (rule conjunct1)
+    show B by (rule conjunct2) assumption
+    show A by (rule conjunct1) assumption
   qed
 qed
 
@@ -171,10 +171,9 @@
   Above, the @{text "conjunct_1/2"} projection rules had to be named
   explicitly, since the goals @{text B} and @{text A} did not provide
   any structural clue.  This may be avoided using \isacommand{from} to
-  focus on @{text prems} (i.e.\ the @{text "A \<and> B"} assumption) as the
-  current facts, enabling the use of double-dot proofs.  Note that
-  \isacommand{from} already does forward-chaining, involving the
-  \name{conjE} rule here.
+  focus on the @{text "A \<and> B"} assumption as the current facts,
+  enabling the use of double-dot proofs.  Note that \isacommand{from}
+  already does forward-chaining, involving the \name{conjE} rule here.
 *}
 
 lemma "A & B --> B & A"
@@ -182,8 +181,8 @@
   assume "A & B"
   show "B & A"
   proof
-    from prems show B ..
-    from prems show A ..
+    from `A & B` show B ..
+    from `A & B` show A ..
   qed
 qed
 
@@ -202,8 +201,8 @@
   assume "A & B"
   then show "B & A"
   proof                    -- {* rule @{text conjE} of @{text "A \<and> B"} *}
-    assume A B
-    show ?thesis ..       -- {* rule @{text conjI} of @{text "B \<and> A"} *}
+    assume B A
+    then show ?thesis ..   -- {* rule @{text conjI} of @{text "B \<and> A"} *}
   qed
 qed
 
@@ -215,10 +214,10 @@
 
 lemma "A & B --> B & A"
 proof
-  assume ab: "A & B"
-  from ab have a: A ..
-  from ab have b: B ..
-  from b a show "B & A" ..
+  assume "A & B"
+  from `A & B` have A ..
+  from `A & B` have B ..
+  from `B` `A` show "B & A" ..
 qed
 
 text {*
@@ -230,12 +229,12 @@
 lemma "A & B --> B & A"
 proof -
   {
-    assume ab: "A & B"
-    from ab have a: A ..
-    from ab have b: B ..
-    from b a have "B & A" ..
+    assume "A & B"
+    from `A & B` have A ..
+    from `A & B` have B ..
+    from `B` `A` have "B & A" ..
   }
-  thus ?thesis ..         -- {* rule \name{impI} *}
+  then show ?thesis ..         -- {* rule \name{impI} *}
 qed
 
 text {*
@@ -258,19 +257,16 @@
 text {*
   For our example the most appropriate way of reasoning is probably
   the middle one, with conjunction introduction done after
-  elimination.  This reads even more concisely using
-  \isacommand{thus}, which abbreviates
-  \isacommand{then}~\isacommand{show}.\footnote{In the same vein,
-  \isacommand{hence} abbreviates \isacommand{then}~\isacommand{have}.}
+  elimination.
 *}
 
 lemma "A & B --> B & A"
 proof
   assume "A & B"
-  thus "B & A"
+  then show "B & A"
   proof
-    assume A B
-    show ?thesis ..
+    assume B A
+    then show ?thesis ..
   qed
 qed
 
@@ -294,13 +290,13 @@
 lemma "P | P --> P"
 proof
   assume "P | P"
-  thus P
+  then show P
   proof                    -- {*
     rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
   *}
-    assume P show P .
+    assume P show P by assumption
   next
-    assume P show P .
+    assume P show P by assumption
   qed
 qed
 
@@ -331,11 +327,11 @@
 lemma "P | P --> P"
 proof
   assume "P | P"
-  thus P
+  then show P
   proof
     assume P
-    show P .
-    show P .
+    show P by assumption
+    show P by assumption
   qed
 qed
 
@@ -349,7 +345,7 @@
 lemma "P | P --> P"
 proof
   assume "P | P"
-  thus P ..
+  then show P ..
 qed
 
 
@@ -372,13 +368,13 @@
 lemma "(EX x. P (f x)) --> (EX y. P y)"
 proof
   assume "EX x. P (f x)"
-  thus "EX y. P y"
+  then show "EX y. P y"
   proof (rule exE)             -- {*
     rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
   *}
     fix a
     assume "P (f a)" (is "P ?witness")
-    show ?thesis by (rule exI [of P ?witness])
+    then show ?thesis by (rule exI [of P ?witness])
   qed
 qed
 
@@ -394,11 +390,11 @@
 lemma "(EX x. P (f x)) --> (EX y. P y)"
 proof
   assume "EX x. P (f x)"
-  thus "EX y. P y"
+  then show "EX y. P y"
   proof
     fix a
     assume "P (f a)"
-    show ?thesis ..
+    then show ?thesis ..
   qed
 qed
 
@@ -413,7 +409,7 @@
 proof
   assume "EX x. P (f x)"
   then obtain a where "P (f a)" ..
-  thus "EX y. P y" ..
+  then show "EX y. P y" ..
 qed
 
 text {*
@@ -443,18 +439,9 @@
   assume r: "A ==> B ==> C"
   show C
   proof (rule r)
-    show A by (rule conjunct1)
-    show B by (rule conjunct2)
+    show A by (rule conjunct1) assumption
+    show B by (rule conjunct2) assumption
   qed
 qed
 
-text {*
-  Note that classic Isabelle handles higher rules in a slightly
-  different way.  The tactic script as given in \cite{isabelle-intro}
-  for the same example of \name{conjE} depends on the primitive
-  \texttt{goal} command to decompose the rule into premises and
-  conclusion.  The actual result would then emerge by discharging of
-  the context at \texttt{qed} time.
-*}
-
 end
diff -r 0035be079bee -r ead82c82da9e src/HOL/Isar_examples/Cantor.thy
--- a/src/HOL/Isar_examples/Cantor.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -34,15 +34,15 @@
   proof
     assume "?S : range f"
     then obtain y where "?S = f y" ..
-    thus False
+    then show False
     proof (rule equalityCE)
       assume "y : f y"
-      assume "y : ?S" hence "y ~: f y" ..
-      thus ?thesis by contradiction
+      assume "y : ?S" then have "y ~: f y" ..
+      with `y : f y` show ?thesis by contradiction
     next
       assume "y ~: ?S"
-      assume "y ~: f y" hence "y : ?S" ..
-      thus ?thesis by contradiction
+      assume "y ~: f y" then have "y : ?S" ..
+      with `y ~: ?S` show ?thesis by contradiction
     qed
   qed
 qed
diff -r 0035be079bee -r ead82c82da9e src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -121,11 +121,14 @@
   case (Cons x xs)
   show ?case
   proof (induct x)
-    case Const show ?case by simp
+    case Const
+    from Cons show ?case by simp
   next
-    case Load show ?case by simp
+    case Load
+    from Cons show ?case by simp
   next
-    case Apply show ?case by simp
+    case Apply
+    from Cons show ?case by simp
   qed
 qed
 
@@ -139,7 +142,7 @@
   next
     case Binop then show ?case by (simp add: exec_append)
   qed
-  thus ?thesis by (simp add: execute_def)
+  then show ?thesis by (simp add: execute_def)
 qed
 
 
diff -r 0035be079bee -r ead82c82da9e src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -43,12 +43,12 @@
     show "(a Un t) Un u : ?T"
     proof -
       have "a Un (t Un u) : ?T"
+	using `a : A`
       proof (rule tiling.Un)
-        show "a : A" .
         from `(a Un t) Int u = {}` have "t Int u = {}" by blast
         then show "t Un u: ?T" by (rule Un)
-        have "a <= - t" .
-        with `(a Un t) Int u = {}` show "a <= - (t Un u)" by blast
+        from `a <= - t` and `(a Un t) Int u = {}`
+	show "a <= - (t Un u)" by blast
       qed
       also have "a Un (t Un u) = (a Un t) Un u"
         by (simp only: Un_assoc)
@@ -201,7 +201,7 @@
   show "?F {}" by (rule finite.emptyI)
   fix a t assume "?F t"
   assume "a : domino" then have "?F a" by (rule domino_finite)
-  then show "?F (a Un t)" by (rule finite_UnI)
+  from this and `?F t` show "?F (a Un t)" by (rule finite_UnI)
 qed
 
 lemma tiling_domino_01:
@@ -223,14 +223,17 @@
     have "?e (a Un t) b = ?e a b Un ?e t b" by (rule evnodd_Un)
     also obtain i j where e: "?e a b = {(i, j)}"
     proof -
+      from `a \<in> domino` and `b < 2`
       have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
       then show ?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))"
     proof (rule card_insert_disjoint)
-      show "finite (?e t b)"
-        by (rule evnodd_finite, rule tiling_domino_finite)
+      from `t \<in> tiling domino` have "finite t"
+	by (rule tiling_domino_finite)
+      then show "finite (?e t b)"
+        by (rule evnodd_finite)
       from e have "(i, j) : ?e a b" by simp
       with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
     qed
diff -r 0035be079bee -r ead82c82da9e src/HOL/Isar_examples/NestedDatatype.thy
--- a/src/HOL/Isar_examples/NestedDatatype.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Isar_examples/NestedDatatype.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -44,12 +44,14 @@
     fix a show "?P (Var a)" by simp
   next
     fix b ts assume "?Q ts"
-    thus "?P (App b ts)" by (simp add: o_def)
+    then show "?P (App b ts)"
+      by (simp only: subst.simps)
   next
     show "?Q []" by simp
   next
     fix t ts
-    assume "?P t" "?Q ts" thus "?Q (t # ts)" by simp
+    assume "?P t" "?Q ts" then show "?Q (t # ts)"
+      by (simp only: subst.simps)
   qed
 qed
 
@@ -64,12 +66,12 @@
   fix a show "P (Var a)" by (rule var)
 next
   fix b t ts assume "list_all P ts"
-  thus "P (App b ts)" by (rule app)
+  then show "P (App b ts)" by (rule app)
 next
   show "list_all P []" by simp
 next
   fix t ts assume "P t" "list_all P ts"
-  thus "list_all P (t # ts)" by simp
+  then show "list_all P (t # ts)" by simp
 qed
 
 lemma
@@ -79,7 +81,7 @@
   show ?case by (simp add: o_def)
 next
   case (App b ts)
-  thus ?case by (induct ts) simp_all
+  then show ?case by (induct ts) simp_all
 qed
 
 end
diff -r 0035be079bee -r ead82c82da9e src/HOL/Isar_examples/Peirce.thy
--- a/src/HOL/Isar_examples/Peirce.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Isar_examples/Peirce.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -21,16 +21,16 @@
 
 theorem "((A --> B) --> A) --> A"
 proof
-  assume aba: "(A --> B) --> A"
+  assume "(A --> B) --> A"
   show A
   proof (rule classical)
     assume "~ A"
     have "A --> B"
     proof
       assume A
-      thus B by contradiction
+      with `~ A` show B by contradiction
     qed
-    with aba show A ..
+    with `(A --> B) --> A` show A ..
   qed
 qed
 
@@ -52,17 +52,17 @@
 
 theorem "((A --> B) --> A) --> A"
 proof
-  assume aba: "(A --> B) --> A"
+  assume "(A --> B) --> A"
   show A
   proof (rule classical)
     presume "A --> B"
-    with aba show A ..
+    with `(A --> B) --> A` show A ..
   next
     assume "~ A"
     show "A --> B"
     proof
       assume A
-      thus B by contradiction
+      with `~ A` show B by contradiction
     qed
   qed
 qed
diff -r 0035be079bee -r ead82c82da9e src/HOL/Lattice/Bounds.thy
--- a/src/HOL/Lattice/Bounds.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Lattice/Bounds.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -147,7 +147,7 @@
     from sup show "is_inf (dual x) (dual y) (dual sup)" ..
     from sup' show "is_inf (dual x) (dual y) (dual sup')" ..
   qed
-  thus "sup = sup'" ..
+  then show "sup = sup'" ..
 qed
 
 theorem is_Inf_uniq: "is_Inf A inf \<Longrightarrow> is_Inf A inf' \<Longrightarrow> inf = inf'"
@@ -159,12 +159,12 @@
     from inf' show "inf \<sqsubseteq> inf'"
     proof (rule is_Inf_greatest)
       fix x assume "x \<in> A"
-      from inf show "inf \<sqsubseteq> x" ..
+      with inf show "inf \<sqsubseteq> x" ..
     qed
     from inf show "inf' \<sqsubseteq> inf"
     proof (rule is_Inf_greatest)
       fix x assume "x \<in> A"
-      from inf' show "inf' \<sqsubseteq> x" ..
+      with inf' show "inf' \<sqsubseteq> x" ..
     qed
   qed
 qed
@@ -177,7 +177,7 @@
     from sup show "is_Inf (dual ` A) (dual sup)" ..
     from sup' show "is_Inf (dual ` A) (dual sup')" ..
   qed
-  thus "sup = sup'" ..
+  then show "sup = sup'" ..
 qed
 
 
@@ -193,8 +193,8 @@
   show ?thesis
   proof
     show "x \<sqsubseteq> x" ..
-    show "x \<sqsubseteq> y" .
-    fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" .
+    show "x \<sqsubseteq> y" by assumption
+    fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by assumption
   qed
 qed
 
@@ -203,10 +203,10 @@
   assume "x \<sqsubseteq> y"
   show ?thesis
   proof
-    show "x \<sqsubseteq> y" .
+    show "x \<sqsubseteq> y" by assumption
     show "y \<sqsubseteq> y" ..
     fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
-    show "y \<sqsubseteq> z" .
+    show "y \<sqsubseteq> z" by assumption
   qed
 qed
 
@@ -233,8 +233,8 @@
       from is_Inf show "z \<sqsubseteq> inf"
       proof (rule is_Inf_greatest)
         fix a assume "a \<in> ?A"
-        hence "a = x \<or> a = y" by blast
-        thus "z \<sqsubseteq> a"
+        then have "a = x \<or> a = y" by blast
+        then show "z \<sqsubseteq> a"
         proof
           assume "a = x"
           with zx show ?thesis by simp
@@ -249,8 +249,8 @@
     show "is_Inf {x, y} inf"
     proof
       fix a assume "a \<in> ?A"
-      hence "a = x \<or> a = y" by blast
-      thus "inf \<sqsubseteq> a"
+      then have "a = x \<or> a = y" by blast
+      then show "inf \<sqsubseteq> a"
       proof
         assume "a = x"
         also from is_inf have "inf \<sqsubseteq> x" ..
@@ -304,12 +304,12 @@
     from is_Inf show "x \<sqsubseteq> sup"
     proof (rule is_Inf_greatest)
       fix y assume "y \<in> ?B"
-      hence "\<forall>a \<in> A. a \<sqsubseteq> y" ..
+      then have "\<forall>a \<in> A. a \<sqsubseteq> y" ..
       from this x show "x \<sqsubseteq> y" ..
     qed
   next
     fix z assume "\<forall>x \<in> A. x \<sqsubseteq> z"
-    hence "z \<in> ?B" ..
+    then have "z \<in> ?B" ..
     with is_Inf show "sup \<sqsubseteq> z" ..
   qed
 qed
@@ -317,14 +317,14 @@
 theorem Sup_Inf: "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf \<Longrightarrow> is_Inf A inf"
 proof -
   assume "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf"
-  hence "is_Inf (dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b}) (dual inf)"
+  then have "is_Inf (dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b}) (dual inf)"
     by (simp only: dual_Inf dual_leq)
   also have "dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b} = {b'. \<forall>a' \<in> dual ` A. a' \<sqsubseteq> b'}"
     by (auto iff: dual_ball dual_Collect simp add: image_Collect)  (* FIXME !? *)
   finally have "is_Inf \<dots> (dual inf)" .
-  hence "is_Sup (dual ` A) (dual inf)"
+  then have "is_Sup (dual ` A) (dual inf)"
     by (rule Inf_Sup)
-  thus ?thesis ..
+  then show ?thesis ..
 qed
 
 end
diff -r 0035be079bee -r ead82c82da9e src/HOL/Lattice/CompleteLattice.thy
--- a/src/HOL/Lattice/CompleteLattice.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Lattice/CompleteLattice.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -22,8 +22,8 @@
 theorem ex_Sup: "\<exists>sup::'a::complete_lattice. is_Sup A sup"
 proof -
   from ex_Inf obtain sup where "is_Inf {b. \<forall>a\<in>A. a \<sqsubseteq> b} sup" by blast
-  hence "is_Sup A sup" by (rule Inf_Sup)
-  thus ?thesis ..
+  then have "is_Sup A sup" by (rule Inf_Sup)
+  then show ?thesis ..
 qed
 
 text {*
@@ -50,8 +50,8 @@
 lemma Meet_equality [elim?]: "is_Inf A inf \<Longrightarrow> \<Sqinter>A = inf"
 proof (unfold Meet_def)
   assume "is_Inf A inf"
-  thus "(THE inf. is_Inf A inf) = inf"
-    by (rule the_equality) (rule is_Inf_uniq)
+  then show "(THE inf. is_Inf A inf) = inf"
+    by (rule the_equality) (rule is_Inf_uniq [OF _ `is_Inf A inf`])
 qed
 
 lemma MeetI [intro?]:
@@ -63,8 +63,8 @@
 lemma Join_equality [elim?]: "is_Sup A sup \<Longrightarrow> \<Squnion>A = sup"
 proof (unfold Join_def)
   assume "is_Sup A sup"
-  thus "(THE sup. is_Sup A sup) = sup"
-    by (rule the_equality) (rule is_Sup_uniq)
+  then show "(THE sup. is_Sup A sup) = sup"
+    by (rule the_equality) (rule is_Sup_uniq [OF _ `is_Sup A sup`])
 qed
 
 lemma JoinI [intro?]:
@@ -82,7 +82,8 @@
 lemma is_Inf_Meet [intro?]: "is_Inf A (\<Sqinter>A)"
 proof (unfold Meet_def)
   from ex_Inf obtain inf where "is_Inf A inf" ..
-  thus "is_Inf A (THE inf. is_Inf A inf)" by (rule theI) (rule is_Inf_uniq)
+  then show "is_Inf A (THE inf. is_Inf A inf)"
+    by (rule theI) (rule is_Inf_uniq [OF _ `is_Inf A inf`])
 qed
 
 lemma Meet_greatest [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> x \<sqsubseteq> a) \<Longrightarrow> x \<sqsubseteq> \<Sqinter>A"
@@ -95,7 +96,8 @@
 lemma is_Sup_Join [intro?]: "is_Sup A (\<Squnion>A)"
 proof (unfold Join_def)
   from ex_Sup obtain sup where "is_Sup A sup" ..
-  thus "is_Sup A (THE sup. is_Sup A sup)" by (rule theI) (rule is_Sup_uniq)
+  then show "is_Sup A (THE sup. is_Sup A sup)"
+    by (rule theI) (rule is_Sup_uniq [OF _ `is_Sup A sup`])
 qed
 
 lemma Join_least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> x) \<Longrightarrow> \<Squnion>A \<sqsubseteq> x"
@@ -122,15 +124,15 @@
   have ge: "f ?a \<sqsubseteq> ?a"
   proof
     fix x assume x: "x \<in> ?H"
-    hence "?a \<sqsubseteq> x" ..
-    hence "f ?a \<sqsubseteq> f x" by (rule mono)
+    then have "?a \<sqsubseteq> x" ..
+    then have "f ?a \<sqsubseteq> f x" by (rule mono)
     also from x have "... \<sqsubseteq> x" ..
     finally show "f ?a \<sqsubseteq> x" .
   qed
   also have "?a \<sqsubseteq> f ?a"
   proof
     from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)
-    thus "f ?a \<in> ?H" ..
+    then show "f ?a \<in> ?H" ..
   qed
   finally show "f ?a = ?a" .
 qed
@@ -153,7 +155,7 @@
 lemma bottom_least [intro?]: "\<bottom> \<sqsubseteq> x"
 proof (unfold bottom_def)
   have "x \<in> UNIV" ..
-  thus "\<Sqinter>UNIV \<sqsubseteq> x" ..
+  then show "\<Sqinter>UNIV \<sqsubseteq> x" ..
 qed
 
 lemma bottomI [intro?]: "(\<And>a. x \<sqsubseteq> a) \<Longrightarrow> \<bottom> = x"
@@ -161,7 +163,7 @@
   assume "\<And>a. x \<sqsubseteq> a"
   show "\<Sqinter>UNIV = x"
   proof
-    fix a show "x \<sqsubseteq> a" .
+    fix a show "x \<sqsubseteq> a" by fact
   next
     fix b :: "'a::complete_lattice"
     assume b: "\<forall>a \<in> UNIV. b \<sqsubseteq> a"
@@ -173,7 +175,7 @@
 lemma top_greatest [intro?]: "x \<sqsubseteq> \<top>"
 proof (unfold top_def)
   have "x \<in> UNIV" ..
-  thus "x \<sqsubseteq> \<Squnion>UNIV" ..
+  then show "x \<sqsubseteq> \<Squnion>UNIV" ..
 qed
 
 lemma topI [intro?]: "(\<And>a. a \<sqsubseteq> x) \<Longrightarrow> \<top> = x"
@@ -181,7 +183,7 @@
   assume "\<And>a. a \<sqsubseteq> x"
   show "\<Squnion>UNIV = x"
   proof
-    fix a show "a \<sqsubseteq> x" .
+    fix a show "a \<sqsubseteq> x" by fact
   next
     fix b :: "'a::complete_lattice"
     assume b: "\<forall>a \<in> UNIV. a \<sqsubseteq> b"
@@ -204,8 +206,8 @@
   show "\<exists>inf'. is_Inf A' inf'"
   proof -
     have "\<exists>sup. is_Sup (undual ` A') sup" by (rule ex_Sup)
-    hence "\<exists>sup. is_Inf (dual ` undual ` A') (dual sup)" by (simp only: dual_Inf)
-    thus ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])
+    then have "\<exists>sup. is_Inf (dual ` undual ` A') (dual sup)" by (simp only: dual_Inf)
+    then show ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])
   qed
 qed
 
@@ -217,15 +219,15 @@
 theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual ` A)"
 proof -
   from is_Inf_Meet have "is_Sup (dual ` A) (dual (\<Sqinter>A))" ..
-  hence "\<Squnion>(dual ` A) = dual (\<Sqinter>A)" ..
-  thus ?thesis ..
+  then have "\<Squnion>(dual ` A) = dual (\<Sqinter>A)" ..
+  then show ?thesis ..
 qed
 
 theorem dual_Join [intro?]: "dual (\<Squnion>A) = \<Sqinter>(dual ` A)"
 proof -
   from is_Sup_Join have "is_Inf (dual ` A) (dual (\<Squnion>A))" ..
-  hence "\<Sqinter>(dual ` A) = dual (\<Squnion>A)" ..
-  thus ?thesis ..
+  then have "\<Sqinter>(dual ` A) = dual (\<Squnion>A)" ..
+  then show ?thesis ..
 qed
 
 text {*
@@ -237,10 +239,10 @@
   have "\<top> = dual \<bottom>"
   proof
     fix a' have "\<bottom> \<sqsubseteq> undual a'" ..
-    hence "dual (undual a') \<sqsubseteq> dual \<bottom>" ..
-    thus "a' \<sqsubseteq> dual \<bottom>" by simp
+    then have "dual (undual a') \<sqsubseteq> dual \<bottom>" ..
+    then show "a' \<sqsubseteq> dual \<bottom>" by simp
   qed
-  thus ?thesis ..
+  then show ?thesis ..
 qed
 
 theorem dual_top [intro?]: "dual \<top> = \<bottom>"
@@ -248,10 +250,10 @@
   have "\<bottom> = dual \<top>"
   proof
     fix a' have "undual a' \<sqsubseteq> \<top>" ..
-    hence "dual \<top> \<sqsubseteq> dual (undual a')" ..
-    thus "dual \<top> \<sqsubseteq> a'" by simp
+    then have "dual \<top> \<sqsubseteq> dual (undual a')" ..
+    then show "dual \<top> \<sqsubseteq> a'" by simp
   qed
-  thus ?thesis ..
+  then show ?thesis ..
 qed
 
 
@@ -267,13 +269,13 @@
 lemma is_inf_binary: "is_inf x y (\<Sqinter>{x, y})"
 proof -
   have "is_Inf {x, y} (\<Sqinter>{x, y})" ..
-  thus ?thesis by (simp only: is_Inf_binary)
+  then show ?thesis by (simp only: is_Inf_binary)
 qed
 
 lemma is_sup_binary: "is_sup x y (\<Squnion>{x, y})"
 proof -
   have "is_Sup {x, y} (\<Squnion>{x, y})" ..
-  thus ?thesis by (simp only: is_Sup_binary)
+  then show ?thesis by (simp only: is_Sup_binary)
 qed
 
 instance complete_lattice \<subseteq> lattice
@@ -302,16 +304,16 @@
   fix a assume "a \<in> A"
   also assume "A \<subseteq> B"
   finally have "a \<in> B" .
-  thus "\<Sqinter>B \<sqsubseteq> a" ..
+  then show "\<Sqinter>B \<sqsubseteq> a" ..
 qed
 
 theorem Join_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
 proof -
   assume "A \<subseteq> B"
-  hence "dual ` A \<subseteq> dual ` B" by blast
-  hence "\<Sqinter>(dual ` B) \<sqsubseteq> \<Sqinter>(dual ` A)" by (rule Meet_subset_antimono)
-  hence "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join)
-  thus ?thesis by (simp only: dual_leq)
+  then have "dual ` A \<subseteq> dual ` B" by blast
+  then have "\<Sqinter>(dual ` B) \<sqsubseteq> \<Sqinter>(dual ` A)" by (rule Meet_subset_antimono)
+  then have "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join)
+  then show ?thesis by (simp only: dual_leq)
 qed
 
 text {*
@@ -321,7 +323,7 @@
 theorem Meet_Un: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
 proof
   fix a assume "a \<in> A \<union> B"
-  thus "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> a"
+  then show "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> a"
   proof
     assume a: "a \<in> A"
     have "\<Sqinter>A \<sqinter> \<Sqinter>B \<sqsubseteq> \<Sqinter>A" ..
@@ -340,13 +342,13 @@
     show "b \<sqsubseteq> \<Sqinter>A"
     proof
       fix a assume "a \<in> A"
-      hence "a \<in>  A \<union> B" ..
+      then have "a \<in>  A \<union> B" ..
       with b show "b \<sqsubseteq> a" ..
     qed
     show "b \<sqsubseteq> \<Sqinter>B"
     proof
       fix a assume "a \<in> B"
-      hence "a \<in>  A \<union> B" ..
+      then have "a \<in>  A \<union> B" ..
       with b show "b \<sqsubseteq> a" ..
     qed
   qed
@@ -370,11 +372,11 @@
 theorem Meet_singleton: "\<Sqinter>{x} = x"
 proof
   fix a assume "a \<in> {x}"
-  hence "a = x" by simp
-  thus "x \<sqsubseteq> a" by (simp only: leq_refl)
+  then have "a = x" by simp
+  then show "x \<sqsubseteq> a" by (simp only: leq_refl)
 next
   fix b assume "\<forall>a \<in> {x}. b \<sqsubseteq> a"
-  thus "b \<sqsubseteq> x" by simp
+  then show "b \<sqsubseteq> x" by simp
 qed
 
 theorem Join_singleton: "\<Squnion>{x} = x"
@@ -392,12 +394,12 @@
 proof
   fix a :: "'a::complete_lattice"
   assume "a \<in> {}"
-  hence False by simp
-  thus "\<Squnion>UNIV \<sqsubseteq> a" ..
+  then have False by simp
+  then show "\<Squnion>UNIV \<sqsubseteq> a" ..
 next
   fix b :: "'a::complete_lattice"
   have "b \<in> UNIV" ..
-  thus "b \<sqsubseteq> \<Squnion>UNIV" ..
+  then show "b \<sqsubseteq> \<Squnion>UNIV" ..
 qed
 
 theorem Join_empty: "\<Squnion>{} = \<Sqinter>UNIV"
diff -r 0035be079bee -r ead82c82da9e src/HOL/Lattice/Lattice.thy
--- a/src/HOL/Lattice/Lattice.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Lattice/Lattice.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -43,8 +43,8 @@
 lemma meet_equality [elim?]: "is_inf x y inf \<Longrightarrow> x \<sqinter> y = inf"
 proof (unfold meet_def)
   assume "is_inf x y inf"
-  thus "(THE inf. is_inf x y inf) = inf"
-    by (rule the_equality) (rule is_inf_uniq)
+  then show "(THE inf. is_inf x y inf) = inf"
+    by (rule the_equality) (rule is_inf_uniq [OF _ `is_inf x y inf`])
 qed
 
 lemma meetI [intro?]:
@@ -54,8 +54,8 @@
 lemma join_equality [elim?]: "is_sup x y sup \<Longrightarrow> x \<squnion> y = sup"
 proof (unfold join_def)
   assume "is_sup x y sup"
-  thus "(THE sup. is_sup x y sup) = sup"
-    by (rule the_equality) (rule is_sup_uniq)
+  then show "(THE sup. is_sup x y sup) = sup"
+    by (rule the_equality) (rule is_sup_uniq [OF _ `is_sup x y sup`])
 qed
 
 lemma joinI [intro?]: "x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow>
@@ -71,7 +71,8 @@
 lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
 proof (unfold meet_def)
   from ex_inf obtain inf where "is_inf x y inf" ..
-  thus "is_inf x y (THE inf. is_inf x y inf)" by (rule theI) (rule is_inf_uniq)
+  then show "is_inf x y (THE inf. is_inf x y inf)"
+    by (rule theI) (rule is_inf_uniq [OF _ `is_inf x y inf`])
 qed
 
 lemma meet_greatest [intro?]: "z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y"
@@ -87,7 +88,8 @@
 lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"
 proof (unfold join_def)
   from ex_sup obtain sup where "is_sup x y sup" ..
-  thus "is_sup x y (THE sup. is_sup x y sup)" by (rule theI) (rule is_sup_uniq)
+  then show "is_sup x y (THE sup. is_sup x y sup)"
+    by (rule theI) (rule is_sup_uniq [OF _ `is_sup x y sup`])
 qed
 
 lemma join_least [intro?]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
@@ -115,16 +117,16 @@
   show "\<exists>inf'. is_inf x' y' inf'"
   proof -
     have "\<exists>sup. is_sup (undual x') (undual y') sup" by (rule ex_sup)
-    hence "\<exists>sup. is_inf (dual (undual x')) (dual (undual y')) (dual sup)"
+    then have "\<exists>sup. is_inf (dual (undual x')) (dual (undual y')) (dual sup)"
       by (simp only: dual_inf)
-    thus ?thesis by (simp add: dual_ex [symmetric])
+    then show ?thesis by (simp add: dual_ex [symmetric])
   qed
   show "\<exists>sup'. is_sup x' y' sup'"
   proof -
     have "\<exists>inf. is_inf (undual x') (undual y') inf" by (rule ex_inf)
-    hence "\<exists>inf. is_sup (dual (undual x')) (dual (undual y')) (dual inf)"
+    then have "\<exists>inf. is_sup (dual (undual x')) (dual (undual y')) (dual inf)"
       by (simp only: dual_sup)
-    thus ?thesis by (simp add: dual_ex [symmetric])
+    then show ?thesis by (simp add: dual_ex [symmetric])
   qed
 qed
 
@@ -136,15 +138,15 @@
 theorem dual_meet [intro?]: "dual (x \<sqinter> y) = dual x \<squnion> dual y"
 proof -
   from is_inf_meet have "is_sup (dual x) (dual y) (dual (x \<sqinter> y))" ..
-  hence "dual x \<squnion> dual y = dual (x \<sqinter> y)" ..
-  thus ?thesis ..
+  then have "dual x \<squnion> dual y = dual (x \<sqinter> y)" ..
+  then show ?thesis ..
 qed
 
 theorem dual_join [intro?]: "dual (x \<squnion> y) = dual x \<sqinter> dual y"
 proof -
   from is_sup_join have "is_inf (dual x) (dual y) (dual (x \<squnion> y))" ..
-  hence "dual x \<sqinter> dual y = dual (x \<squnion> y)" ..
-  thus ?thesis ..
+  then have "dual x \<sqinter> dual y = dual (x \<squnion> y)" ..
+  then show ?thesis ..
 qed
 
 
@@ -179,7 +181,7 @@
   proof
     show "w \<sqsubseteq> x"
     proof -
-      have "w \<sqsubseteq> x \<sqinter> y" .
+      have "w \<sqsubseteq> x \<sqinter> y" by fact
       also have "\<dots> \<sqsubseteq> x" ..
       finally show ?thesis .
     qed
@@ -187,11 +189,11 @@
     proof
       show "w \<sqsubseteq> y"
       proof -
-        have "w \<sqsubseteq> x \<sqinter> y" .
+        have "w \<sqsubseteq> x \<sqinter> y" by fact
         also have "\<dots> \<sqsubseteq> y" ..
         finally show ?thesis .
       qed
-      show "w \<sqsubseteq> z" .
+      show "w \<sqsubseteq> z" by fact
     qed
   qed
 qed
@@ -211,8 +213,8 @@
 proof
   show "y \<sqinter> x \<sqsubseteq> x" ..
   show "y \<sqinter> x \<sqsubseteq> y" ..
-  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
-  show "z \<sqsubseteq> y \<sqinter> x" ..
+  fix z assume "z \<sqsubseteq> y" and "z \<sqsubseteq> x"
+  then show "z \<sqsubseteq> y \<sqinter> x" ..
 qed
 
 theorem join_commute: "x \<squnion> y = y \<squnion> x"
@@ -230,16 +232,16 @@
   show "x \<sqsubseteq> x" ..
   show "x \<sqsubseteq> x \<squnion> y" ..
   fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> x \<squnion> y"
-  show "z \<sqsubseteq> x" .
+  show "z \<sqsubseteq> x" by assumption
 qed
 
 theorem join_meet_absorb: "x \<squnion> (x \<sqinter> y) = x"
 proof -
   have "dual x \<sqinter> (dual x \<squnion> dual y) = dual x"
     by (rule meet_join_absorb)
-  hence "dual (x \<squnion> (x \<sqinter> y)) = dual x"
+  then have "dual (x \<squnion> (x \<sqinter> y)) = dual x"
     by (simp only: dual_meet dual_join)
-  thus ?thesis ..
+  then show ?thesis ..
 qed
 
 text {*
@@ -258,9 +260,9 @@
 proof -
   have "dual x \<sqinter> dual x = dual x"
     by (rule meet_idem)
-  hence "dual (x \<squnion> x) = dual x"
+  then have "dual (x \<squnion> x) = dual x"
     by (simp only: dual_join)
-  thus ?thesis ..
+  then show ?thesis ..
 qed
 
 text {*
@@ -271,14 +273,15 @@
 proof
   assume "x \<sqsubseteq> y"
   show "x \<sqsubseteq> x" ..
-  show "x \<sqsubseteq> y" .
-  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" .
+  show "x \<sqsubseteq> y" by fact
+  fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y"
+  show "z \<sqsubseteq> x" by fact
 qed
 
 theorem join_related [elim?]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
 proof -
-  assume "x \<sqsubseteq> y" hence "dual y \<sqsubseteq> dual x" ..
-  hence "dual y \<sqinter> dual x = dual y" by (rule meet_related)
+  assume "x \<sqsubseteq> y" then have "dual y \<sqsubseteq> dual x" ..
+  then have "dual y \<sqinter> dual x = dual y" by (rule meet_related)
   also have "dual y \<sqinter> dual x = dual (y \<squnion> x)" by (simp only: dual_join)
   also have "y \<squnion> x = x \<squnion> y" by (rule join_commute)
   finally show ?thesis ..
@@ -295,8 +298,8 @@
 theorem meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
 proof
   assume "x \<sqsubseteq> y"
-  hence "is_inf x y x" ..
-  thus "x \<sqinter> y = x" ..
+  then have "is_inf x y x" ..
+  then show "x \<sqinter> y = x" ..
 next
   have "x \<sqinter> y \<sqsubseteq> y" ..
   also assume "x \<sqinter> y = x"
@@ -306,8 +309,8 @@
 theorem join_connection: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
 proof
   assume "x \<sqsubseteq> y"
-  hence "is_sup x y y" ..
-  thus "x \<squnion> y = y" ..
+  then have "is_sup x y y" ..
+  then show "x \<squnion> y = y" ..
 next
   have "x \<sqsubseteq> x \<squnion> y" ..
   also assume "x \<squnion> y = y"
@@ -555,27 +558,27 @@
     assume "a \<sqsubseteq> c" have "a \<sqinter> b \<sqsubseteq> c \<sqinter> b"
     proof
       have "a \<sqinter> b \<sqsubseteq> a" ..
-      also have "\<dots> \<sqsubseteq> c" .
+      also have "\<dots> \<sqsubseteq> c" by fact
       finally show "a \<sqinter> b \<sqsubseteq> c" .
       show "a \<sqinter> b \<sqsubseteq> b" ..
     qed
   } note this [elim?]
-  assume "x \<sqsubseteq> z" hence "x \<sqinter> y \<sqsubseteq> z \<sqinter> y" ..
+  assume "x \<sqsubseteq> z" then have "x \<sqinter> y \<sqsubseteq> z \<sqinter> y" ..
   also have "\<dots> = y \<sqinter> z" by (rule meet_commute)
-  also assume "y \<sqsubseteq> w" hence "y \<sqinter> z \<sqsubseteq> w \<sqinter> z" ..
+  also assume "y \<sqsubseteq> w" then have "y \<sqinter> z \<sqsubseteq> w \<sqinter> z" ..
   also have "\<dots> = z \<sqinter> w" by (rule meet_commute)
   finally show ?thesis .
 qed
 
 theorem join_mono: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> w \<Longrightarrow> x \<squnion> y \<sqsubseteq> z \<squnion> w"
 proof -
-  assume "x \<sqsubseteq> z" hence "dual z \<sqsubseteq> dual x" ..
-  moreover assume "y \<sqsubseteq> w" hence "dual w \<sqsubseteq> dual y" ..
+  assume "x \<sqsubseteq> z" then have "dual z \<sqsubseteq> dual x" ..
+  moreover assume "y \<sqsubseteq> w" then have "dual w \<sqsubseteq> dual y" ..
   ultimately have "dual z \<sqinter> dual w \<sqsubseteq> dual x \<sqinter> dual y"
     by (rule meet_mono)
-  hence "dual (z \<squnion> w) \<sqsubseteq> dual (x \<squnion> y)"
+  then have "dual (z \<squnion> w) \<sqsubseteq> dual (x \<squnion> y)"
     by (simp only: dual_join)
-  thus ?thesis ..
+  then show ?thesis ..
 qed
 
 text {*
@@ -590,8 +593,8 @@
 proof
   assume morph: "\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
   fix x y :: "'a::lattice"
-  assume "x \<sqsubseteq> y" hence "x \<sqinter> y = x" ..
-  hence "x = x \<sqinter> y" ..
+  assume "x \<sqsubseteq> y" then have "x \<sqinter> y = x" ..
+  then have "x = x \<sqinter> y" ..
   also have "f \<dots> \<sqsubseteq> f x \<sqinter> f y" by (rule morph)
   also have "\<dots> \<sqsubseteq> f y" ..
   finally show "f x \<sqsubseteq> f y" .
@@ -602,8 +605,8 @@
     fix x y
     show "f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
     proof
-      have "x \<sqinter> y \<sqsubseteq> x" .. thus "f (x \<sqinter> y) \<sqsubseteq> f x" by (rule mono)
-      have "x \<sqinter> y \<sqsubseteq> y" .. thus "f (x \<sqinter> y) \<sqsubseteq> f y" by (rule mono)
+      have "x \<sqinter> y \<sqsubseteq> x" .. then show "f (x \<sqinter> y) \<sqsubseteq> f x" by (rule mono)
+      have "x \<sqinter> y \<sqsubseteq> y" .. then show "f (x \<sqinter> y) \<sqsubseteq> f y" by (rule mono)
     qed
   qed
 qed
diff -r 0035be079bee -r ead82c82da9e src/HOL/Library/AssocList.thy
--- a/src/HOL/Library/AssocList.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Library/AssocList.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -19,7 +19,7 @@
 fun
   delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
-  "delete k [] = []"
+    "delete k [] = []"
   | "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
 
 fun
@@ -79,27 +79,25 @@
 fun
   restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
-  "restrict A [] = []"
+    "restrict A [] = []"
   | "restrict A (p#ps) = (if fst p \<in> A then p#restrict A ps else restrict A ps)"
 
 fun
   map_ran :: "('key \<Rightarrow> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
-  "map_ran f [] = []"
+    "map_ran f [] = []"
   | "map_ran f (p#ps) = (fst p, f (fst p) (snd p)) # map_ran f ps"
 
 fun
   clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
-  "clearjunk [] = []"  
+    "clearjunk [] = []"  
   | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
 
 lemmas [simp del] = compose_hint
 
 
-(* ******************************************************************************** *)
 subsection {* Lookup *}
-(* ******************************************************************************** *)
 
 lemma lookup_simps [code func]: 
   "map_of [] k = None"
@@ -107,9 +105,7 @@
   by simp_all
 
 
-(* ******************************************************************************** *)
 subsection {* @{const delete} *}
-(* ******************************************************************************** *)
 
 lemma delete_def:
   "delete k xs = filter (\<lambda>p. fst p \<noteq> k) xs"
@@ -140,7 +136,7 @@
 lemma distinct_delete:
   assumes "distinct (map fst al)" 
   shows "distinct (map fst (delete k al))"
-using prems
+using assms
 proof (induct al)
   case Nil thus ?case by simp
 next
@@ -152,7 +148,7 @@
   show ?case
   proof (cases "fst a = k")
     case True
-    from True dist_al show ?thesis by simp
+    with Cons dist_al show ?thesis by simp
   next
     case False
     from dist_al
@@ -171,9 +167,8 @@
 lemma clearjunk_delete: "clearjunk (delete x al) = delete x (clearjunk al)"
   by (induct al rule: clearjunk.induct) (auto simp add: delete_idem delete_twist)
 
-(* ******************************************************************************** *)
+
 subsection {* @{const clearjunk} *}
-(* ******************************************************************************** *)
 
 lemma insert_fst_filter: 
   "insert a(fst ` {x \<in> set ps. fst x \<noteq> a}) = insert a (fst ` set ps)"
@@ -221,9 +216,8 @@
 lemma clearjunk_idem: "clearjunk (clearjunk al) = clearjunk al"
   by simp
 
-(* ******************************************************************************** *)
+
 subsection {* @{const dom} and @{term "ran"} *}
-(* ******************************************************************************** *)
 
 lemma dom_map_of': "fst ` set al = dom (map_of al)"
   by (induct al) auto
@@ -295,9 +289,8 @@
   finally show ?thesis .
 qed
    
-(* ******************************************************************************** *)
+
 subsection {* @{const update} *}
-(* ******************************************************************************** *)
 
 lemma update_conv: "map_of (update k v al) k' = ((map_of al)(k\<mapsto>v)) k'"
   by (induct al) auto
@@ -311,7 +304,7 @@
 lemma distinct_update:
   assumes "distinct (map fst al)" 
   shows "distinct (map fst (update k v al))"
-using prems
+using assms
 proof (induct al)
   case Nil thus ?case by simp
 next
@@ -374,9 +367,7 @@
   by (simp add: update_conv' image_map_upd)
 
 
-(* ******************************************************************************** *)
 subsection {* @{const updates} *}
-(* ******************************************************************************** *)
 
 lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
 proof (induct ks arbitrary: vs al)
@@ -401,7 +392,7 @@
 lemma distinct_updates:
   assumes "distinct (map fst al)"
   shows "distinct (map fst (updates ks vs al))"
-  using prems
+  using assms
   by (induct ks arbitrary: vs al)
    (auto simp add: distinct_update split: list.splits)
 
@@ -447,9 +438,8 @@
   "size xs = size ys \<Longrightarrow> updates xs (ys@zs) al = updates xs ys al"
   by (induct xs arbitrary: ys al) (auto split: list.splits)
 
-(* ******************************************************************************** *)
+
 subsection {* @{const map_ran} *}
-(* ******************************************************************************** *)
 
 lemma map_ran_conv: "map_of (map_ran f al) k = option_map (f k) (map_of al k)"
   by (induct al) auto
@@ -466,9 +456,8 @@
 lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
   by (induct al rule: clearjunk.induct) (auto simp add: delete_def map_ran_filter)
 
-(* ******************************************************************************** *)
+
 subsection {* @{const merge} *}
-(* ******************************************************************************** *)
 
 lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
   by (induct ys arbitrary: xs) (auto simp add: dom_update)
@@ -476,7 +465,7 @@
 lemma distinct_merge:
   assumes "distinct (map fst xs)"
   shows "distinct (map fst (merge xs ys))"
-  using prems
+  using assms
 by (induct ys arbitrary: xs) (auto simp add: dom_merge distinct_update)
 
 lemma clearjunk_merge:
@@ -536,14 +525,13 @@
 lemma merge_append: "map_of (xs@ys) = map_of (merge ys xs)"
   by (simp add: merge_conv')
 
-(* ******************************************************************************** *)
+
 subsection {* @{const compose} *}
-(* ******************************************************************************** *)
 
 lemma compose_first_None [simp]: 
   assumes "map_of xs k = None" 
   shows "map_of (compose xs ys) k = None"
-using prems by (induct xs ys rule: compose.induct)
+using assms by (induct xs ys rule: compose.induct)
   (auto split: option.splits split_if_asm)
 
 lemma compose_conv: 
@@ -591,7 +579,7 @@
 lemma compose_first_Some [simp]:
   assumes "map_of xs k = Some v" 
   shows "map_of (compose xs ys) k = map_of ys v"
-using prems by (simp add: compose_conv)
+using assms by (simp add: compose_conv)
 
 lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
 proof (induct xs ys rule: compose.induct)
@@ -623,7 +611,7 @@
 lemma distinct_compose:
  assumes "distinct (map fst xs)"
  shows "distinct (map fst (compose xs ys))"
-using prems
+using assms
 proof (induct xs ys rule: compose.induct)
   case 1 thus ?case by simp
 next
@@ -695,9 +683,7 @@
   by (simp add: compose_conv map_comp_None_iff)
 
 
-(* ******************************************************************************** *)
 subsection {* @{const restrict} *}
-(* ******************************************************************************** *)
 
 lemma restrict_def:
   "restrict A = filter (\<lambda>p. fst p \<in> A)"
diff -r 0035be079bee -r ead82c82da9e src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Library/BigO.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -282,7 +282,7 @@
     apply (subst func_diff)
     apply (rule bigo_abs)
     done
-  also have "... <= O(h)"
+  also from a have "... <= O(h)"
     by (rule bigo_elt_subset)
   finally show "(%x. abs (f x) - abs (g x)) : O(h)".
 qed
diff -r 0035be079bee -r ead82c82da9e src/HOL/Library/Graphs.thy
--- a/src/HOL/Library/Graphs.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Library/Graphs.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -3,7 +3,7 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
-header ""
+header ""   (* FIXME proper header *)
 
 theory Graphs
 imports Main SCT_Misc Kleene_Algebras ExecutableSet
@@ -56,8 +56,8 @@
 lemma graph_ext:
   assumes "\<And>n e n'. has_edge G n e n' = has_edge H n e n'"
   shows "G = H"
-  using prems
-  by (cases G, cases H, auto simp:split_paired_all has_edge_def)
+  using assms
+  by (cases G, cases H) (auto simp:split_paired_all has_edge_def)
 
 
 instance graph :: (type, type) "{comm_monoid_add}"
@@ -219,7 +219,7 @@
 lemma graph_leqI:
   assumes "\<And>n e n'. has_edge G n e n' \<Longrightarrow> has_edge H n e n'"
   shows "G \<le> H"
-  using prems
+  using assms
   unfolding graph_leq_def has_edge_def
   by auto
 
@@ -229,18 +229,18 @@
   assumes "has_edge G n e n' \<Longrightarrow> P"
   assumes "has_edge H n e n' \<Longrightarrow> P"
   shows P
-  using prems
+  using assms
   by (auto simp: in_grplus)
 
 lemma 
   assumes "x \<in> S k"
   shows "x \<in> (\<Union>k. S k)"
-  using prems by blast
+  using assms by blast
 
 lemma graph_union_least:
   assumes "\<And>n. Graph (G n) \<le> C"
   shows "Graph (\<Union>n. G n) \<le> C"
-  using prems unfolding graph_leq_def
+  using assms unfolding graph_leq_def
   by auto
 
 lemma Sup_graph_eq:
@@ -333,15 +333,15 @@
 lemma endnode_nth:
   assumes "length (snd p) = Suc k"
   shows "end_node p = snd (snd (path_nth p k))"
-  using prems unfolding end_node_def path_nth_def
+  using assms unfolding end_node_def path_nth_def
   by auto
 
 lemma path_nth_graph:
   assumes "k < length (snd p)"
   assumes "has_fpath G p"
   shows "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p k)"
-  using prems
-proof (induct k arbitrary:p)
+using assms
+proof (induct k arbitrary: p)
   case 0 thus ?case 
     unfolding path_nth_def by (auto elim:has_fpath.cases)
 next
@@ -364,7 +364,7 @@
 lemma path_nth_connected:
   assumes "Suc k < length (snd p)"
   shows "fst (path_nth p (Suc k)) = snd (snd (path_nth p k))"
-  using prems
+  using assms
   unfolding path_nth_def
   by auto
 
@@ -399,9 +399,9 @@
     hence "fst (path_nth p (Suc i mod ?l)) = fst (path_nth p 0)" 
       by (simp add: mod_Suc)
     also from fst_p0 have "\<dots> = fst p" .
-    also have "\<dots> = end_node p" .
+    also have "\<dots> = end_node p" by assumption
     also have "\<dots> = snd (snd (path_nth p ?k))" 
-      by (auto simp:endnode_nth wrap)
+      by (auto simp: endnode_nth wrap)
     finally show ?thesis .
   qed
 qed
@@ -411,17 +411,21 @@
   and loop: "fst p = end_node p"
   and nonempty: "0 < length (snd p)" (is "0 < ?l")
   shows "has_ipath G (omega p)"
-proof (auto simp:has_ipath_def)
-  fix i 
-  from `0 < ?l` have "i mod ?l < ?l" (is "?k < ?l")
-    by simp
-  with path_nth_graph 
-  have pk_G: "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p ?k)" .
+proof -
+  {
+    fix i 
+    from `0 < ?l` have "i mod ?l < ?l" (is "?k < ?l")
+      by simp
+    from this and `has_fpath G p`
+    have pk_G: "(\<lambda>(n,e,n'). has_edge G n e n') (path_nth p ?k)"
+      by (rule path_nth_graph)
 
-  from path_loop_connect[OF loop nonempty] pk_G
-  show "has_edge G (fst (omega p i)) (snd (omega p i)) (fst (omega p (Suc i)))"
-    unfolding path_loop_def has_edge_def split_def
-    by simp
+    from path_loop_connect[OF loop nonempty] pk_G
+    have "has_edge G (fst (omega p i)) (snd (omega p i)) (fst (omega p (Suc i)))"
+      unfolding path_loop_def has_edge_def split_def
+      by simp
+  }
+  then show ?thesis by (auto simp:has_ipath_def)
 qed
 
 definition prod :: "('n, 'e::monoid_mult) fpath \<Rightarrow> 'e"
@@ -514,7 +518,7 @@
 lemma upto_append[simp]:
   assumes "i \<le> j" "j \<le> k"
   shows "[ i ..< j ] @ [j ..< k] = [i ..< k]"
-  using prems and upt_add_eq_append[of i j "k - j"]
+  using assms and upt_add_eq_append[of i j "k - j"]
   by simp
 
 lemma foldr_monoid: "foldr (op *) xs 1 * foldr (op *) ys 1
@@ -525,7 +529,7 @@
   assumes "i < j"
   assumes "j < k"
   shows "prod (p\<langle>i,k\<rangle>) = prod (p\<langle>i,j\<rangle>) * prod (p\<langle>j,k\<rangle>)"
-  using prems
+  using assms
   unfolding prod_def sub_path_def
   by (simp add:map_compose[symmetric] comp_def)
    (simp only:foldr_monoid map_append[symmetric] upto_append)
@@ -535,7 +539,7 @@
   assumes "length es = l"
   assumes "has_fpath G (n,es)"
   shows "has_edge (G ^ l) n (prod (n,es)) (end_node (n,es))"
-using prems
+using assms
 proof (induct l arbitrary:n es)
   case 0 thus ?case
     by (simp add:in_grunit end_node_def) 
@@ -679,7 +683,7 @@
 
 lemma sub_path_loop:
   assumes "0 < k"
-  assumes k:"k = length (snd loop)"
+  assumes k: "k = length (snd loop)"
   assumes loop: "fst loop = end_node loop"
   shows "(omega loop)\<langle>k * i,k * Suc i\<rangle> = loop" (is "?\<omega> = loop")
 proof (rule prod_eqI)
@@ -698,14 +702,17 @@
       = snd (snd (path_nth loop (i mod k)))"
       unfolding k
       apply (rule path_loop_connect[OF loop])
-      by (insert prems, auto)
+      using `0 < k` and k
+      apply auto
+      done
 
     from `j < k` 
     show "snd ?\<omega> ! j = snd loop ! j"
       unfolding sub_path_def
       apply (simp add:path_loop_def split_def add_ac)
       apply (simp add:a k[symmetric])
-      by (simp add:path_nth_def)
+      apply (simp add:path_nth_def)
+      done
   qed
 qed
 
diff -r 0035be079bee -r ead82c82da9e src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -450,7 +450,7 @@
       proof (elim exE disjE conjE)
         fix M assume "?R M M0" and N: "N = M + {#a#}"
         from acc_hyp have "?R M M0 --> ?W (M + {#a#})" ..
-        then have "?W (M + {#a#})" ..
+        from this and `?R M M0` have "?W (M + {#a#})" ..
         then show "?W N" by (simp only: N)
       next
         fix K
@@ -487,23 +487,23 @@
     from wf have "\<forall>M \<triangleright> ?W. ?W (M + {#a#})"
     proof induct
       fix a
-      assume "!!b. r b a ==> \<forall>M \<triangleright> ?W. ?W (M + {#b#})"
+      assume r: "!!b. r b a ==> \<forall>M \<triangleright> ?W. ?W (M + {#b#})"
       show "\<forall>M \<triangleright> ?W. ?W (M + {#a#})"
       proof
         fix M assume "?W M"
         then show "?W (M + {#a#})"
-          by (rule acc_induct) (rule tedious_reasoning)
+          by (rule acc_induct) (rule tedious_reasoning [OF _ r])
       qed
     qed
-    then show "?W (M + {#a#})" ..
+    from this and `?W M` show "?W (M + {#a#})" ..
   qed
 qed
 
 theorem wf_mult1: "wfP r ==> wfP (mult1 r)"
-  by (rule acc_wfI, rule all_accessible)
+  by (rule acc_wfI) (rule all_accessible)
 
 theorem wf_mult: "wfP r ==> wfP (mult r)"
-  by (unfold mult_def, rule wfP_trancl, rule wf_mult1)
+  unfolding mult_def by (rule wfP_trancl) (rule wf_mult1)
 
 
 subsubsection {* Closure-free presentation *}
@@ -511,7 +511,7 @@
 (*Badly needed: a linear arithmetic procedure for multisets*)
 
 lemma diff_union_single_conv: "a :# J ==> I + J - {#a#} = I + (J - {#a#})"
-by (simp add: multiset_eq_conv_count_eq)
+  by (simp add: multiset_eq_conv_count_eq)
 
 text {* One direction. *}
 
@@ -548,7 +548,7 @@
   done
 
 lemma elem_imp_eq_diff_union: "a :# M ==> M = M - {#a#} + {#a#}"
-by (simp add: multiset_eq_conv_count_eq)
+  by (simp add: multiset_eq_conv_count_eq)
 
 lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \<exists>a N. M = N + {#a#}"
   apply (erule size_eq_Suc_imp_elem [THEN exE])
@@ -588,8 +588,7 @@
 lemma one_step_implies_mult:
   "J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. r k j
     ==> mult r (I + K) (I + J)"
-  apply (insert one_step_implies_mult_aux, blast)
-  done
+  using one_step_implies_mult_aux by blast
 
 
 subsubsection {* Partial-order properties *}
@@ -609,9 +608,7 @@
 
 lemma mult_irrefl_aux:
     "finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) \<Longrightarrow> A = {}"
-  apply (induct rule: finite_induct)
-   apply (auto intro: order_less_trans)
-  done
+  by (induct rule: finite_induct) (auto intro: order_less_trans)
 
 lemma mult_less_not_refl: "\<not> M < (M::'a::order multiset)"
   apply (unfold less_multiset_def, auto)
@@ -621,15 +618,13 @@
   done
 
 lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R"
-by (insert mult_less_not_refl, fast)
+  using insert mult_less_not_refl by fast
 
 
 text {* Transitivity. *}
 
 theorem mult_less_trans: "K < M ==> M < N ==> K < (N::'a::order multiset)"
-  apply (unfold less_multiset_def mult_def)
-  apply (blast intro: trancl_trans')
-  done
+  unfolding less_multiset_def mult_def by (blast intro: trancl_trans')
 
 text {* Asymmetry. *}
 
diff -r 0035be079bee -r ead82c82da9e src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Library/Quotient.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -31,27 +31,27 @@
 
 lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
 proof -
-  assume "\<not> (x \<sim> y)" thus "\<not> (y \<sim> x)"
+  assume "\<not> (x \<sim> y)" then show "\<not> (y \<sim> x)"
     by (rule contrapos_nn) (rule equiv_sym)
 qed
 
 lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))"
 proof -
-  assume "\<not> (x \<sim> y)" and yz: "y \<sim> z"
+  assume "\<not> (x \<sim> y)" and "y \<sim> z"
   show "\<not> (x \<sim> z)"
   proof
     assume "x \<sim> z"
-    also from yz have "z \<sim> y" ..
+    also from `y \<sim> z` have "z \<sim> y" ..
     finally have "x \<sim> y" .
-    thus False by contradiction
+    with `\<not> (x \<sim> y)` show False by contradiction
   qed
 qed
 
 lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))"
 proof -
-  assume "\<not> (y \<sim> z)" hence "\<not> (z \<sim> y)" ..
-  also assume "x \<sim> y" hence "y \<sim> x" ..
-  finally have "\<not> (z \<sim> x)" . thus "(\<not> x \<sim> z)" ..
+  assume "\<not> (y \<sim> z)" then have "\<not> (z \<sim> y)" ..
+  also assume "x \<sim> y" then have "y \<sim> x" ..
+  finally have "\<not> (z \<sim> x)" . then show "(\<not> x \<sim> z)" ..
 qed
 
 text {*
@@ -80,9 +80,9 @@
 theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
 proof (cases A)
   fix R assume R: "A = Abs_quot R"
-  assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast
+  assume "R \<in> quot" then have "\<exists>a. R = {x. a \<sim> x}" by blast
   with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
-  thus ?thesis unfolding class_def .
+  then show ?thesis unfolding class_def .
 qed
 
 lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
@@ -105,8 +105,8 @@
       by (simp only: class_def Abs_quot_inject quotI)
     moreover have "a \<sim> a" ..
     ultimately have "a \<in> {x. b \<sim> x}" by blast
-    hence "b \<sim> a" by blast
-    thus ?thesis ..
+    then have "b \<sim> a" by blast
+    then show ?thesis ..
   qed
 next
   assume ab: "a \<sim> b"
@@ -125,7 +125,7 @@
         finally show "a \<sim> x" .
       qed
     qed
-    thus ?thesis by (simp only: class_def)
+    then show ?thesis by (simp only: class_def)
   qed
 qed
 
@@ -142,15 +142,15 @@
   proof (rule someI2)
     show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
     fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
-    hence "a \<sim> x" .. thus "x \<sim> a" ..
+    then have "a \<sim> x" .. then show "x \<sim> a" ..
   qed
 qed
 
 theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A"
 proof (cases A)
   fix a assume a: "A = \<lfloor>a\<rfloor>"
-  hence "pick A \<sim> a" by (simp only: pick_equiv)
-  hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..
+  then have "pick A \<sim> a" by (simp only: pick_equiv)
+  then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..
   with a show ?thesis by simp
 qed
 
@@ -175,7 +175,7 @@
     moreover
     show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" ..
     moreover
-    show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" .
+    show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" by (rule P)
     ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:)
   qed
   finally show ?thesis .
diff -r 0035be079bee -r ead82c82da9e src/HOL/Library/SCT_Misc.thy
--- a/src/HOL/Library/SCT_Misc.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Library/SCT_Misc.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -3,9 +3,9 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
-header ""
+header ""   (* FIXME proper header *)
 
-theory SCT_Misc
+theory SCT_Misc   (* FIXME proper name *)
 imports Main
 begin
 
@@ -95,11 +95,13 @@
   "section_of s n = (LEAST i. n < s (Suc i))"
 
 lemma section_help:
-  assumes [intro, simp]: "increasing s"
+  assumes "increasing s"
   shows "\<exists>i. n < s (Suc i)" 
 proof -
-  from increasing_inc have "n \<le> s n" .
-  also from increasing_strict have "\<dots> < s (Suc n)" by simp
+  have "n \<le> s n"
+    using `increasing s` by (rule increasing_inc)
+  also have "\<dots> < s (Suc n)"
+    using `increasing s` increasing_strict by simp
   finally show ?thesis ..
 qed
 
@@ -107,7 +109,7 @@
   assumes "increasing s"
   shows "n < s (Suc (section_of s n))"
   unfolding section_of_def
-  by (rule LeastI_ex) (rule section_help)
+  by (rule LeastI_ex) (rule section_help [OF `increasing s`])
 
 lemma section_of1:
   assumes [simp, intro]: "increasing s"
diff -r 0035be079bee -r ead82c82da9e src/HOL/Library/SCT_Theorem.thy
--- a/src/HOL/Library/SCT_Theorem.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Library/SCT_Theorem.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -3,7 +3,7 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
-header ""
+header ""   (* FIXME proper header *)
 
 theory SCT_Theorem
 imports Main Ramsey SCT_Misc SCT_Definition
@@ -795,10 +795,9 @@
       unfolding is_desc_fthread_def
       by auto
 
-    have "i < s (Suc ?k)" by (rule section_of2)
-    also have "\<dots> \<le> s j" 
-      by (rule increasing_weak[of s], assumption)
-    (insert `?k < j`, arith)
+    have "i < s (Suc ?k)" by (rule section_of2) simp
+    also have "\<dots> \<le> s j"
+      by (rule increasing_weak [of s], assumption) (insert `?k < j`, arith)
     also note `\<dots> \<le> l`
     finally have "i < l" .
     with desc
@@ -925,10 +924,10 @@
       {
 	fix x assume r: "x \<in> section s ?L"
 	
-	have e1: "max (s (Suc i)) n < s (Suc ?K)" by (rule section_of2)
+	have e1: "max (s (Suc i)) n < s (Suc ?K)" by (rule section_of2) simp
         note `s (Suc ?K) < j`
         also have "j < s (Suc ?L)"
-          by (rule section_of2)
+          by (rule section_of2) simp
         finally have "Suc ?K \<le> ?L"
           by (simp add:increasing_bij)          
 	with increasing_weak have "s (Suc ?K) \<le> s ?L" by simp
@@ -1074,12 +1073,12 @@
   "set2list = inv set"
 
 lemma finite_set2list: 
-  assumes [intro]: "finite S" 
+  assumes "finite S" 
   shows "set (set2list S) = S"
   unfolding set2list_def 
 proof (rule f_inv_f)
-  from finite_list
-  have "\<exists>l. set l = S" .
+  from `finite S` have "\<exists>l. set l = S"
+    by (rule finite_list)
   thus "S \<in> range set"
     unfolding image_def
     by auto
@@ -1307,7 +1306,7 @@
       by (simp only:split_conv, rule a, auto)
 
     obtain n H m where
-      G_struct: "G = (n, H, m)" by (cases G) simp
+      G_struct: "G = (n, H, m)" by (cases G)
 
     let ?s = "enumerate S"
     let ?q = "contract ?s p"
@@ -1381,7 +1380,7 @@
 proof -
   from fin obtain P where b: "bounded_acg P A"
     unfolding finite_acg_def ..
-  show ?thesis using LJA_Theorem4[OF b]
+  show ?thesis using LJA_Theorem4[OF b] and `SCT' A`
     by simp
 qed
 
diff -r 0035be079bee -r ead82c82da9e src/HOL/Matrix/MatrixGeneral.thy
--- a/src/HOL/Matrix/MatrixGeneral.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -85,7 +85,8 @@
     next
       fix y
       assume hyp: "Rep_matrix x (fst y) (snd y) \<noteq> 0"
-      show "\<exists> a b. (Rep_matrix x b a \<noteq> 0 & y = (b,a))" by (rule exI[of _ "snd y"], rule exI[of _ "fst y"], simp)
+      show "\<exists> a b. (Rep_matrix x b a \<noteq> 0 & y = (b,a))"
+	by (rule exI[of _ "snd y"], rule exI[of _ "fst y"]) (simp add: hyp)
     qed
   then have "finite (?swap`?A)"
     proof -
diff -r 0035be079bee -r ead82c82da9e src/HOL/NumberTheory/Euler.thy
--- a/src/HOL/NumberTheory/Euler.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/NumberTheory/Euler.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -264,7 +264,7 @@
     by (auto simp add: zEven_def zOdd_def)
   then have aux_1: "2 * ((p - 1) div 2) = (p - 1)"
     by (auto simp add: even_div_2_prop2)
-  then have "1 < (p - 1)"
+  with `2 < p` have "1 < (p - 1)"
     by auto
   then have " 1 < (2 * ((p - 1) div 2))"
     by (auto simp add: aux_1)
diff -r 0035be079bee -r ead82c82da9e src/HOL/NumberTheory/Quadratic_Reciprocity.thy
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -115,8 +115,8 @@
    (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
 proof -
   assume "a \<in> zOdd"
-  from QRLemma4 have
-    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)"..
+  from QRLemma4 [OF this] have
+    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" ..
   moreover have "0 \<le> int(card E)"
     by auto
   moreover have "0 \<le> setsum (%x. ((x * a) div p)) A"
diff -r 0035be079bee -r ead82c82da9e src/HOL/W0/W0.thy
--- a/src/HOL/W0/W0.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/W0/W0.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -405,7 +405,7 @@
   then have "map ($ s) a |- Var n :: map ($ s) a ! n"
     by (rule has_type.Var)
   also have "map ($ s) a ! n = $ s (a ! n)"
-    by (rule nth_map)
+    by (rule nth_map) (rule Var)
   also have "map ($ s) a = $ s a"
     by (simp only: app_subst_list)
   finally show ?case .
diff -r 0035be079bee -r ead82c82da9e src/HOL/ex/Commutative_Ring_Complete.thy
--- a/src/HOL/ex/Commutative_Ring_Complete.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/ex/Commutative_Ring_Complete.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -150,7 +150,7 @@
     then obtain d where X:"x=Suc (Suc d)" ..
     from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
     with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
-    with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp
+    with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp assumption
     with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
   ultimately show ?case by blast
 next
@@ -168,7 +168,7 @@
     then obtain d where X:"x=Suc (Suc d)" ..
     from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
     with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
-    with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp
+    with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp assumption
     with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
   ultimately show ?case by blast
 next
diff -r 0035be079bee -r ead82c82da9e src/HOL/ex/Higher_Order_Logic.thy
--- a/src/HOL/ex/Higher_Order_Logic.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -58,7 +58,7 @@
 theorem sym [sym]: "x = y \<Longrightarrow> y = x"
 proof -
   assume "x = y"
-  thus "y = x" by (rule subst) (rule refl)
+  then show "y = x" by (rule subst) (rule refl)
 qed
 
 lemma [trans]: "x = y \<Longrightarrow> P y \<Longrightarrow> P x"
@@ -110,7 +110,7 @@
 theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"
 proof (unfold false_def)
   assume "\<forall>A. A"
-  thus A ..
+  then show A ..
 qed
 
 theorem trueI [intro]: \<top>
@@ -121,7 +121,7 @@
 theorem notI [intro]: "(A \<Longrightarrow> \<bottom>) \<Longrightarrow> \<not> A"
 proof (unfold not_def)
   assume "A \<Longrightarrow> \<bottom>"
-  thus "A \<longrightarrow> \<bottom>" ..
+  then show "A \<longrightarrow> \<bottom>" ..
 qed
 
 theorem notE [elim]: "\<not> A \<Longrightarrow> A \<Longrightarrow> B"
@@ -129,7 +129,7 @@
   assume "A \<longrightarrow> \<bottom>"
   also assume A
   finally have \<bottom> ..
-  thus B ..
+  then show B ..
 qed
 
 lemma notE': "A \<Longrightarrow> \<not> A \<Longrightarrow> B"
@@ -145,8 +145,8 @@
     fix C show "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
     proof
       assume "A \<longrightarrow> B \<longrightarrow> C"
-      also have A .
-      also have B .
+      also note `A`
+      also note `B`
       finally show C .
     qed
   qed
@@ -161,7 +161,7 @@
     also have "A \<longrightarrow> B \<longrightarrow> A"
     proof
       assume A
-      thus "B \<longrightarrow> A" ..
+      then show "B \<longrightarrow> A" ..
     qed
     finally have A .
   } moreover {
@@ -182,9 +182,9 @@
     fix C show "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
     proof
       assume "A \<longrightarrow> C"
-      also have A .
+      also note `A`
       finally have C .
-      thus "(B \<longrightarrow> C) \<longrightarrow> C" ..
+      then show "(B \<longrightarrow> C) \<longrightarrow> C" ..
     qed
   qed
 qed
@@ -199,7 +199,7 @@
       show "(B \<longrightarrow> C) \<longrightarrow> C"
       proof
         assume "B \<longrightarrow> C"
-        also have B .
+        also note `B`
         finally show C .
       qed
     qed
@@ -213,11 +213,11 @@
   from c have "(A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C" ..
   also have "A \<longrightarrow> C"
   proof
-    assume A thus C by (rule r1)
+    assume A then show C by (rule r1)
   qed
   also have "B \<longrightarrow> C"
   proof
-    assume B thus C by (rule r2)
+    assume B then show C by (rule r2)
   qed
   finally show C .
 qed
@@ -230,8 +230,8 @@
     fix C show "(\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
     proof
       assume "\<forall>x. P x \<longrightarrow> C"
-      hence "P a \<longrightarrow> C" ..
-      also have "P a" .
+      then have "P a \<longrightarrow> C" ..
+      also note `P a`
       finally show C .
     qed
   qed
@@ -247,7 +247,7 @@
     fix x show "P x \<longrightarrow> C"
     proof
       assume "P x"
-      thus C by (rule r)
+      then show C by (rule r)
     qed
   qed
   finally show C .
@@ -269,7 +269,7 @@
     have "A \<longrightarrow> B"
     proof
       assume A
-      thus B by (rule contradiction)
+      with `\<not> A` show B by (rule contradiction)
     qed
     with a show A ..
   qed
@@ -282,7 +282,7 @@
   show A
   proof (rule classical)
     assume "\<not> A"
-    thus ?thesis by (rule contradiction)
+    with `\<not> \<not> A` show ?thesis by (rule contradiction)
   qed
 qed
 
@@ -294,11 +294,11 @@
     assume "\<not> (A \<or> \<not> A)"
     have "\<not> A"
     proof
-      assume A hence "A \<or> \<not> A" ..
-      thus \<bottom> by (rule contradiction)
+      assume A then have "A \<or> \<not> A" ..
+      with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction)
     qed
-    hence "A \<or> \<not> A" ..
-    thus \<bottom> by (rule contradiction)
+    then have "A \<or> \<not> A" ..
+    with `\<not> (A \<or> \<not> A)` show \<bottom> by (rule contradiction)
   qed
 qed
 
@@ -309,10 +309,10 @@
   from tertium_non_datur show C
   proof
     assume A
-    thus ?thesis by (rule r1)
+    then show ?thesis by (rule r1)
   next
     assume "\<not> A"
-    thus ?thesis by (rule r2)
+    then show ?thesis by (rule r2)
   qed
 qed
 
@@ -321,9 +321,9 @@
   assume r: "\<not> A \<Longrightarrow> A"
   show A
   proof (rule classical_cases)
-    assume A thus A .
+    assume A then show A .
   next
-    assume "\<not> A" thus A by (rule r)
+    assume "\<not> A" then show A by (rule r)
   qed
 qed
 
diff -r 0035be079bee -r ead82c82da9e src/HOL/ex/PER.thy
--- a/src/HOL/ex/PER.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/ex/PER.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -242,7 +242,7 @@
   proof (rule someI2)
     show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
     fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
-    then have "a \<sim> x" ..
+    from this and a have "a \<sim> x" ..
     then show "x \<sim> a" ..
   qed
 qed
diff -r 0035be079bee -r ead82c82da9e src/HOL/ex/ThreeDivides.thy
--- a/src/HOL/ex/ThreeDivides.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/ex/ThreeDivides.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -77,7 +77,7 @@
   let ?thr = "(3::nat)"
   have "?thr dvd 9" by simp
   moreover
-  have "?thr dvd (10*(10^n - 1))" by (rule dvd_mult)
+  have "?thr dvd (10*(10^n - 1))" by (rule dvd_mult) (rule Suc)
   hence "?thr dvd (10^(n+1) - 10)" by (simp add: nat_distrib)
   ultimately
   have"?thr dvd ((10^(n+1) - 10) + 9)"
diff -r 0035be079bee -r ead82c82da9e src/HOL/ex/Unification.thy
--- a/src/HOL/ex/Unification.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/ex/Unification.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -461,7 +461,7 @@
     by (rule acc_downward) (rule unify_rel.intros)
   hence no_new_vars: 
     "\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
-    by (rule unify_vars)
+    by (rule unify_vars) (rule `unify M M' = Some \<theta>1`)
 
   from ih2 show ?case 
   proof