# HG changeset patch
# User wenzelm
# Date 1469178043 -7200
# Node ID f8652d0534fa80ba6204c67bb7cf6b9cb2910d85
# Parent  70d4d9e5707b23d4d20c91aa63ff153e6e0deda8
tuned proofs -- avoid unstructured calculation;

diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Archimedean_Field.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -395,9 +395,9 @@
       by blast
     then have l: "l = - r"
       by simp
-    moreover with \<open>l \<noteq> 0\<close> False have "r > 0"
+    with \<open>l \<noteq> 0\<close> False have "r > 0"
       by simp
-    ultimately show ?thesis
+    with l show ?thesis
       using pos_mod_bound [of r]
       by (auto simp add: zmod_zminus2_eq_if less_le field_simps intro: floor_unique)
   qed
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Cardinals/Ordinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -310,11 +310,11 @@
   have minim[simp]: "minim r' (Field r') \<in> Field r'"
     using wo_rel.minim_inField[unfolded wo_rel_def, OF WELL' _ r'] by auto
   { fix b
-    assume "(b, minim r' (Field r')) \<in> r'"
-    moreover hence "b \<in> Field r'" unfolding Field_def by auto
+    assume b: "(b, minim r' (Field r')) \<in> r'"
+    hence "b \<in> Field r'" unfolding Field_def by auto
     hence "(minim r' (Field r'), b) \<in> r'"
       using wo_rel.minim_least[unfolded wo_rel_def, OF WELL' subset_refl] r' by auto
-    ultimately have "b = minim r' (Field r')"
+    with b have "b = minim r' (Field r')"
       by (metis WELL' antisym_def linear_order_on_def partial_order_on_def well_order_on_def)
   } note * = this
   have 1: "Well_order (r *o r')" using assms by (auto simp add: oprod_Well_order)
@@ -772,9 +772,9 @@
             have "G \<subseteq> fin_support r.zero (Field s)"
             unfolding FinFunc_def fin_support_def proof safe
               fix g assume "g \<in> G"
-              with GF obtain f where "f \<in> F" "g = f(z := r.zero)" by auto
-              moreover with SUPPF have "finite (SUPP f)" by blast
-              ultimately show "finite (SUPP g)"
+              with GF obtain f where f: "f \<in> F" "g = f(z := r.zero)" by auto
+              with SUPPF have "finite (SUPP f)" by blast
+              with f show "finite (SUPP g)"
                 by (elim finite_subset[rotated]) (auto simp: support_def)
             qed
             moreover from F GF zField have "G \<subseteq> Func (Field s) (Field r)"
@@ -831,13 +831,12 @@
                   case True
                   with f have "f(z := r.zero) \<in> G" unfolding G_def by blast
                   with g0(2) f0z have "(f0(z := r.zero), f(z := r.zero)) \<in> oexp" by auto
-                  hence "(f0(z := r.zero, z := x0), f(z := r.zero, z := x0)) \<in> oexp"
+                  hence oexp: "(f0(z := r.zero, z := x0), f(z := r.zero, z := x0)) \<in> oexp"
                     by (elim fun_upd_same_oexp[OF _ _ zField x0Field]) simp
-                  moreover
                   with f F(1) x0min True
                     have "(f(z := x0), f) \<in> oexp" unfolding G_def r.isMinim_def
                     by (intro fun_upd_smaller_oexp[OF _ zField x0Field]) auto
-                  ultimately show ?thesis using transD[OF oexp_trans, of f0 "f(z := x0)" f]
+                  with oexp show ?thesis using transD[OF oexp_trans, of f0 "f(z := x0)" f]
                     unfolding f0_def by auto
                 next
                   case False note notG = this
@@ -1336,10 +1335,9 @@
       hence max_Field: "t.max_fun_diff h (F g) \<in> {a \<in> Field t. h a \<noteq> F g a}"
         by (rule rt.max_fun_diff_in[OF _ gh(2,3)])
       { assume *: "t.max_fun_diff h (F g) \<notin> f ` Field s"
-        with max_Field have "F g (t.max_fun_diff h (F g)) = r.zero" unfolding F_def by auto
-        moreover
+        with max_Field have **: "F g (t.max_fun_diff h (F g)) = r.zero" unfolding F_def by auto
         with * gh(4) have "h (t.max_fun_diff h (F g)) = r.zero" unfolding Let_def by auto
-        ultimately have False using max_Field gh(2,3) unfolding FinFunc_def Func_def by auto
+        with ** have False using max_Field gh(2,3) unfolding FinFunc_def Func_def by auto
       }
       hence max_f_Field: "t.max_fun_diff h (F g) \<in> f ` Field s" by blast
       { fix z assume z: "z \<in> Field t - f ` Field s"
@@ -1433,7 +1431,6 @@
           with f inj have neq: "?f h \<noteq> ?f g"
             unfolding fun_eq_iff inj_on_def rt.oexp_def map_option_case FinFunc_def Func_def Let_def
             by simp metis
-          moreover
           with hg have "t.max_fun_diff (?f h) (?f g) = t.max_fun_diff h g" unfolding rt.oexp_def
             using rt.max_fun_diff[OF \<open>h \<noteq> g\<close>] rt.max_fun_diff_in[OF \<open>h \<noteq> g\<close>]
             by (subst t.max_fun_diff_def, intro t.maxim_equality)
@@ -1441,7 +1438,7 @@
           with Field_fg Field_fh hg fz f_underS compat neq have "(?f h, ?f g) \<in> st.oexp"
              using rt.max_fun_diff[OF \<open>h \<noteq> g\<close>] rt.max_fun_diff_in[OF \<open>h \<noteq> g\<close>] unfolding st.Field_oexp
              unfolding rt.oexp_def st.oexp_def Let_def compat_def by auto
-          ultimately show "?f h \<in> underS (s ^o t) (?f g)" unfolding underS_def by auto
+          with neq show "?f h \<in> underS (s ^o t) (?f g)" unfolding underS_def by auto
         qed
         ultimately have "?f g \<in> Field (s ^o t) \<and> ?f ` underS (r ^o t) g \<subseteq> underS (s ^o t) (?f g)"
           by blast
@@ -1609,12 +1606,12 @@
     have **: "(\<Union>g \<in> fg ` Field t. rs.SUPP g) =
               (\<Union>g \<in> fg ` Field t - {rs.const}. rs.SUPP g)"
       unfolding support_def by auto
-    from * have "\<forall>g \<in> fg ` Field t. finite (rs.SUPP g)" "finite (rst.SUPP fg)"
+    from * have ***: "\<forall>g \<in> fg ` Field t. finite (rs.SUPP g)" "finite (rst.SUPP fg)"
       unfolding rs.Field_oexp FinFunc_def Func_def fin_support_def Option.these_def by force+
-    moreover hence "finite (fg ` Field t - {rs.const})" using *
+    hence "finite (fg ` Field t - {rs.const})" using *
       unfolding support_def rs.zero_oexp[OF Field] FinFunc_def Func_def
       by (elim finite_surj[of _ _ fg]) (fastforce simp: image_iff Option.these_def)
-    ultimately have "finite ((\<Union>g \<in> fg ` Field t. rs.SUPP g) \<times> rst.SUPP fg)"
+    with *** have "finite ((\<Union>g \<in> fg ` Field t. rs.SUPP g) \<times> rst.SUPP fg)"
       by (subst **) (auto intro!: finite_cartesian_product)
     with * show "?g \<in> FinFunc r (s *o t)"
       unfolding Field_oprod rs.Field_oexp FinFunc_def Func_def fin_support_def Option.these_def
@@ -1680,8 +1677,9 @@
           ordIso_transitive[OF oone_ordIso_oexp[OF ordIso_symmetric[OF oone_ordIso] t] oone_ordIso])
   next
      case False
-     moreover hence "s *o t \<noteq> {}" unfolding oprod_def Field_def by fastforce
-     ultimately show ?thesis using \<open>r = {}\<close> ozero_ordIso
+     hence "s *o t \<noteq> {}" unfolding oprod_def Field_def by fastforce
+     with False show ?thesis
+       using \<open>r = {}\<close> ozero_ordIso
        by (auto simp add: s t oprod_Well_order ozero_def)
   qed
 next
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Cardinals/Wellorder_Constructions.thy
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -606,13 +606,13 @@
 
 lemma not_isSucc_zero: "\<not> isSucc zero"
 proof
-  assume "isSucc zero"
-  moreover
+  assume *: "isSucc zero"
   then obtain i where "aboveS i \<noteq> {}" and 1: "minim (Field r) = succ i"
   unfolding isSucc_def zero_def by auto
   hence "succ i \<in> Field r" by auto
-  ultimately show False by (metis REFL isSucc_def minim_least refl_on_domain
-    subset_refl succ_in succ_not_in zero_def)
+  with * show False
+    by (metis REFL isSucc_def minim_least refl_on_domain
+        subset_refl succ_in succ_not_in zero_def)
 qed
 
 lemma isLim_zero[simp]: "isLim zero"
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -505,19 +505,23 @@
 
 instance
 proof
-  fix x :: nat and X :: "nat set"
-  { assume "x \<in> X" "bdd_below X" then show "Inf X \<le> x"
-      by (simp add: Inf_nat_def Least_le) }
-  { assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> x \<le> y" then show "x \<le> Inf X"
-      unfolding Inf_nat_def ex_in_conv[symmetric] by (rule LeastI2_ex) }
-  { assume "x \<in> X" "bdd_above X" then show "x \<le> Sup X"
-      by (simp add: Sup_nat_def bdd_above_nat) }
-  { assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x"
-    moreover then have "bdd_above X"
+  fix x :: nat
+  fix X :: "nat set"
+  show "Inf X \<le> x" if "x \<in> X" "bdd_below X"
+    using that by (simp add: Inf_nat_def Least_le)
+  show "x \<le> Inf X" if "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> x \<le> y"
+    using that unfolding Inf_nat_def ex_in_conv[symmetric] by (rule LeastI2_ex)
+  show "x \<le> Sup X" if "x \<in> X" "bdd_above X"
+    using that by (simp add: Sup_nat_def bdd_above_nat)
+  show "Sup X \<le> x" if "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x"
+  proof -
+    from that have "bdd_above X"
       by (auto simp: bdd_above_def)
-    ultimately show "Sup X \<le> x"
-      by (simp add: Sup_nat_def bdd_above_nat) }
+    with that show ?thesis 
+      by (simp add: Sup_nat_def bdd_above_nat)
+  qed
 qed
+
 end
 
 instantiation int :: conditionally_complete_linorder
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Corec_Examples/LFilter.thy
--- a/src/HOL/Corec_Examples/LFilter.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Corec_Examples/LFilter.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -30,7 +30,6 @@
   from this(1,2) obtain a where "P (lhd ((ltl ^^ a) xs))"
     by (atomize_elim, induct x xs rule: llist.set_induct)
        (auto simp: funpow_Suc_right simp del: funpow.simps(2) intro: exI[of _ 0] exI[of _ "Suc i" for i])
-  moreover
   with \<open>\<not> P (lhd xs)\<close>
     have "(LEAST n. P (lhd ((ltl ^^ n) xs))) = Suc (LEAST n. P (lhd ((ltl ^^ Suc n) xs)))"
     by (intro Least_Suc) auto
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Corec_Examples/Tests/Misc_Mono.thy
--- a/src/HOL/Corec_Examples/Tests/Misc_Mono.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/Misc_Mono.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -382,7 +382,6 @@
   from this(1,2) obtain a where "P (head ((tail ^^ a) xs))"
     by (atomize_elim, induct xs x rule: llist_in.induct) (auto simp: funpow_Suc_right
       simp del: funpow.simps(2) intro: exI[of _ 0] exI[of _ "Suc i" for i])
-  moreover
   with \<open>\<not> P (head xs)\<close>
     have "(LEAST n. P (head ((tail ^^ n) xs))) = Suc (LEAST n. P (head ((tail ^^ Suc n) xs)))"
     by (intro Least_Suc) auto
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Filter.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -489,9 +489,9 @@
   assumes **: "\<And>i P. i \<in> I \<Longrightarrow> \<forall>\<^sub>F x in F i. P x \<Longrightarrow> \<forall>\<^sub>F x in F' i. T P x"
   shows "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x"
 proof -
-  from * obtain X where "finite X" "X \<subseteq> I" "\<forall>\<^sub>F x in \<Sqinter>i\<in>X. F i. P x"
+  from * obtain X where X: "finite X" "X \<subseteq> I" "\<forall>\<^sub>F x in \<Sqinter>i\<in>X. F i. P x"
     unfolding eventually_INF[of _ _ I] by auto
-  moreover then have "eventually (T P) (INFIMUM X F')"
+  then have "eventually (T P) (INFIMUM X F')"
     apply (induction X arbitrary: P)
     apply (auto simp: eventually_inf T2)
     subgoal for x S P Q R
@@ -501,7 +501,7 @@
       apply (auto intro: T1) []
       done
     done
-  ultimately show "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x"
+  with X show "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x"
     by (subst eventually_INF) auto
 qed
 
@@ -798,9 +798,10 @@
   shows "(\<forall>\<^sub>F (x, y) in A \<times>\<^sub>F B. P x) \<longleftrightarrow> (\<forall>\<^sub>F x in A. P x)"
   unfolding eventually_prod_filter
 proof safe
-  fix R Q assume "\<forall>\<^sub>F x in A. R x" "\<forall>\<^sub>F x in B. Q x" "\<forall>x y. R x \<longrightarrow> Q y \<longrightarrow> P x"
-  moreover with \<open>B \<noteq> bot\<close> obtain y where "Q y" by (auto dest: eventually_happens)
-  ultimately show "eventually P A"
+  fix R Q
+  assume *: "\<forall>\<^sub>F x in A. R x" "\<forall>\<^sub>F x in B. Q x" "\<forall>x y. R x \<longrightarrow> Q y \<longrightarrow> P x"
+  with \<open>B \<noteq> bot\<close> obtain y where "Q y" by (auto dest: eventually_happens)
+  with * show "eventually P A"
     by (force elim: eventually_mono)
 next
   assume "eventually P A"
@@ -813,9 +814,10 @@
   shows "(\<forall>\<^sub>F (x, y) in A \<times>\<^sub>F B. P y) \<longleftrightarrow> (\<forall>\<^sub>F y in B. P y)"
   unfolding eventually_prod_filter
 proof safe
-  fix R Q assume "\<forall>\<^sub>F x in A. R x" "\<forall>\<^sub>F x in B. Q x" "\<forall>x y. R x \<longrightarrow> Q y \<longrightarrow> P y"
-  moreover with \<open>A \<noteq> bot\<close> obtain x where "R x" by (auto dest: eventually_happens)
-  ultimately show "eventually P B"
+  fix R Q
+  assume *: "\<forall>\<^sub>F x in A. R x" "\<forall>\<^sub>F x in B. Q x" "\<forall>x y. R x \<longrightarrow> Q y \<longrightarrow> P y"
+  with \<open>A \<noteq> bot\<close> obtain x where "R x" by (auto dest: eventually_happens)
+  with * show "eventually P B"
     by (force elim: eventually_mono)
 next
   assume "eventually P B"
@@ -827,35 +829,40 @@
   fixes F :: "'a \<Rightarrow> 'b filter"
   assumes *: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. F k \<le> F i \<sqinter> F j"
   shows "(INF i:I. F i) = bot \<longleftrightarrow> (\<exists>i\<in>I. F i = bot)"
-proof cases
-  assume "\<exists>i\<in>I. F i = bot"
-  moreover then have "(INF i:I. F i) \<le> bot"
+proof (cases "\<exists>i\<in>I. F i = bot")
+  case True
+  then have "(INF i:I. F i) \<le> bot"
     by (auto intro: INF_lower2)
-  ultimately show ?thesis
+  with True show ?thesis
     by (auto simp: bot_unique)
 next
-  assume **: "\<not> (\<exists>i\<in>I. F i = bot)"
+  case False
   moreover have "(INF i:I. F i) \<noteq> bot"
-  proof cases
-    assume "I \<noteq> {}"
+  proof (cases "I = {}")
+    case True
+    then show ?thesis
+      by (auto simp add: filter_eq_iff)
+  next
+    case False': False
     show ?thesis
     proof (rule INF_filter_not_bot)
-      fix J assume "finite J" "J \<subseteq> I"
+      fix J
+      assume "finite J" "J \<subseteq> I"
       then have "\<exists>k\<in>I. F k \<le> (\<Sqinter>i\<in>J. F i)"
-      proof (induction J)
-        case empty then show ?case
+      proof (induct J)
+        case empty
+        then show ?case
           using \<open>I \<noteq> {}\<close> by auto
       next
         case (insert i J)
-        moreover then obtain k where "k \<in> I" "F k \<le> (\<Sqinter>i\<in>J. F i)" by auto
-        moreover note *[of i k]
-        ultimately show ?case
+        then obtain k where "k \<in> I" "F k \<le> (\<Sqinter>i\<in>J. F i)" by auto
+        with insert *[of i k] show ?case
           by auto
       qed
-      with ** show "(\<Sqinter>i\<in>J. F i) \<noteq> \<bottom>"
+      with False show "(\<Sqinter>i\<in>J. F i) \<noteq> \<bottom>"
         by (auto simp: bot_unique)
     qed
-  qed (auto simp add: filter_eq_iff)
+  qed
   ultimately show ?thesis
     by auto
 qed
@@ -883,9 +890,9 @@
   shows "A \<times>\<^sub>F B \<le> C \<times>\<^sub>F D \<longleftrightarrow> A \<le> C \<and> B \<le> D"
 proof safe
   assume *: "A \<times>\<^sub>F B \<le> C \<times>\<^sub>F D"
-  moreover with assms have "A \<times>\<^sub>F B \<noteq> bot"
+  with assms have "A \<times>\<^sub>F B \<noteq> bot"
     by (auto simp: bot_unique prod_filter_eq_bot)
-  ultimately have "C \<times>\<^sub>F D \<noteq> bot"
+  with * have "C \<times>\<^sub>F D \<noteq> bot"
     by (auto simp: bot_unique)
   then have nCD: "C \<noteq> bot" "D \<noteq> bot"
     by (auto simp: prod_filter_eq_bot)
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -317,14 +317,17 @@
 proof -
   define Sseq where "Sseq = rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})"
   define pick where "pick n = (SOME e. e \<in> Sseq n)" for n
-  { fix n have "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" by (induct n) (auto simp add: Sseq_def inf) }
-  moreover then have *: "\<And>n. pick n \<in> Sseq n"
+  have *: "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" for n
+    by (induct n) (auto simp add: Sseq_def inf)
+  then have **: "\<And>n. pick n \<in> Sseq n"
     unfolding pick_def by (subst (asm) finite.simps) (auto simp add: ex_in_conv intro: someI_ex)
-  ultimately have "range pick \<subseteq> S" by auto
+  with * have "range pick \<subseteq> S" by auto
   moreover
-  { fix n m
-    have "pick n \<notin> Sseq (n + Suc m)" by (induct m) (auto simp add: Sseq_def pick_def)
-    with * have "pick n \<noteq> pick (n + Suc m)" by auto
+  {
+    fix n m
+    have "pick n \<notin> Sseq (n + Suc m)"
+      by (induct m) (auto simp add: Sseq_def pick_def)
+    with ** have "pick n \<noteq> pick (n + Suc m)" by auto
   }
   then have "inj pick" by (intro linorder_injI) (auto simp add: less_iff_Suc_add)
   ultimately show ?thesis by blast
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/IMP/Compiler2.thy
--- a/src/HOL/IMP/Compiler2.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/IMP/Compiler2.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -366,9 +366,8 @@
     rest: "P @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^k (n, s', stk')"
     by auto
   from step `size P \<le> i`
-  have "P' \<turnstile> (i - size P, s, stk) \<rightarrow> (i' - size P, s'', stk'')" 
+  have *: "P' \<turnstile> (i - size P, s, stk) \<rightarrow> (i' - size P, s'', stk'')" 
     by (rule exec1_drop_left)
-  moreover
   then have "i' - size P \<in> succs P' 0"
     by (fastforce dest!: succs_iexec1 simp: exec1_def simp del: iexec.simps)
   with `exits P' \<subseteq> {0..}`
@@ -376,8 +375,7 @@
   from rest this `exits P' \<subseteq> {0..}`     
   have "P' \<turnstile> (i' - size P, s'', stk'') \<rightarrow>^k (n - size P, s', stk')"
     by (rule Suc.IH)
-  ultimately
-  show ?case by auto
+  with * show ?case by auto
 qed
 
 lemmas exec_n_drop_Cons = 
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/IMP/Def_Init_Small.thy
--- a/src/HOL/IMP/Def_Init_Small.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/IMP/Def_Init_Small.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -58,10 +58,9 @@
   "(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c A \<Longrightarrow> EX A'. D (dom s') c' A' & A <= A'"
 proof (induction arbitrary: A rule: small_step_induct)
   case (While b c s)
-  then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
-  moreover
+  then obtain A' where A': "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
   then obtain A'' where "D A' c A''" by (metis D_incr D_mono)
-  ultimately have "D (dom s) (IF b THEN c;; WHILE b DO c ELSE SKIP) (dom s)"
+  with A' have "D (dom s) (IF b THEN c;; WHILE b DO c ELSE SKIP) (dom s)"
     by (metis D.If[OF `vars b \<subseteq> dom s` D.Seq[OF `D (dom s) c A'` D.While[OF _ `D A' c A''`]] D.Skip] D_incr Int_absorb1 subset_trans)
   thus ?case by (metis D_incr `A = dom s`)
 next
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Inductive.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -270,10 +270,10 @@
   show "g (lfp (\<lambda>x. f (g x))) \<le> lfp (\<lambda>x. g (f x))"
   proof (rule lfp_greatest)
     fix u
-    assume "g (f u) \<le> u"
-    moreover then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)"
+    assume u: "g (f u) \<le> u"
+    then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)"
       by (intro assms[THEN monoD] lfp_lowerbound)
-    ultimately show "g (lfp (\<lambda>x. f (g x))) \<le> u"
+    with u show "g (lfp (\<lambda>x. f (g x))) \<le> u"
       by auto
   qed
 qed
@@ -307,10 +307,11 @@
     by (rule gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric])
   show "gfp (\<lambda>x. g (f x)) \<le> g (gfp (\<lambda>x. f (g x)))"
   proof (rule gfp_least)
-    fix u assume "u \<le> g (f u)"
-    moreover then have "g (f u) \<le> g (gfp (\<lambda>x. f (g x)))"
+    fix u
+    assume u: "u \<le> g (f u)"
+    then have "g (f u) \<le> g (gfp (\<lambda>x. f (g x)))"
       by (intro assms[THEN monoD] gfp_upperbound)
-    ultimately show "u \<le> g (gfp (\<lambda>x. f (g x)))"
+    with u show "u \<le> g (gfp (\<lambda>x. f (g x)))"
       by auto
   qed
 qed
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
--- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -7,7 +7,9 @@
 
 section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close>
 
-theory Bourbaki_Witt_Fixpoint imports Main begin
+theory Bourbaki_Witt_Fixpoint
+  imports Main
+begin
 
 lemma ChainsI [intro?]:
   "(\<And>a b. \<lbrakk> a \<in> Y; b \<in> Y \<rbrakk> \<Longrightarrow> (a, b) \<in> r \<or> (b, a) \<in> r) \<Longrightarrow> Y \<in> Chains r"
@@ -131,10 +133,10 @@
         with Sup.IH[OF z] \<open>y = a\<close> Sup.hyps(3)[OF z]
         show ?thesis by(auto dest: iterates_above_ge intro: a)
       next
-        assume "y \<in> iterates_above (f a)"
-        moreover with increasing[OF a] have "y \<in> Field leq"
+        assume *: "y \<in> iterates_above (f a)"
+        with increasing[OF a] have "y \<in> Field leq"
           by(auto dest!: iterates_above_Field intro: FieldI2)
-        ultimately show ?thesis using y by(auto)
+        with * show ?thesis using y by auto
       qed
     qed
     thus ?thesis by simp
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Library/Continuum_Not_Denumerable.thy
--- a/src/HOL/Library/Continuum_Not_Denumerable.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Continuum_Not_Denumerable.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -153,11 +153,11 @@
   assumes "a < b" and "countable A"
   shows "\<exists>x\<in>{a<..<b}. x \<notin> A"
 proof -
-  from \<open>countable A\<close> have "countable (A \<inter> {a<..<b})"
+  from \<open>countable A\<close> have *: "countable (A \<inter> {a<..<b})"
     by auto
-  moreover with \<open>a < b\<close> have "\<not> countable {a<..<b}"
+  with \<open>a < b\<close> have "\<not> countable {a<..<b}"
     by (simp add: uncountable_open_interval)
-  ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}"
+  with * have "A \<inter> {a<..<b} \<noteq> {a<..<b}"
     by auto
   then have "A \<inter> {a<..<b} \<subset> {a<..<b}"
     by (intro psubsetI) auto
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Library/Discrete.thy
--- a/src/HOL/Library/Discrete.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Discrete.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -28,11 +28,13 @@
   assume "n > 0"
   show "P n"
   proof (cases "n = 1")
-    case True with one show ?thesis by simp
+    case True
+    with one show ?thesis by simp
   next
-    case False with \<open>n > 0\<close> have "n \<ge> 2" by auto
-    moreover with * have "P (n div 2)" .
-    ultimately show ?thesis by (rule double)
+    case False
+    with \<open>n > 0\<close> have "n \<ge> 2" by auto
+    with * have "P (n div 2)" .
+    with \<open>n \<ge> 2\<close> show ?thesis by (rule double)
   qed
 qed
   
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -1067,11 +1067,11 @@
   fix x y :: ereal assume xy: "0 \<le> x" "0 \<le> y" "x < y"
   moreover
   from ereal_dense3[OF \<open>x < y\<close>]
-  obtain r where "x < ereal (real_of_rat r)" "ereal (real_of_rat r) < y"
+  obtain r where r: "x < ereal (real_of_rat r)" "ereal (real_of_rat r) < y"
     by auto
-  moreover then have "0 \<le> r"
+  then have "0 \<le> r"
     using le_less_trans[OF \<open>0 \<le> x\<close> \<open>x < ereal (real_of_rat r)\<close>] by auto
-  ultimately show "\<exists>r. x < (sup 0 \<circ> ereal) (real_of_rat r) \<and> (sup 0 \<circ> ereal) (real_of_rat r) < y"
+  with r show "\<exists>r. x < (sup 0 \<circ> ereal) (real_of_rat r) \<and> (sup 0 \<circ> ereal) (real_of_rat r) < y"
     by (intro exI[of _ r]) (auto simp: max_absorb2)
 qed
 
@@ -1172,11 +1172,11 @@
       from ennreal_Ex_less_of_nat[OF r] guess n .. note n = this
       have "\<not> (X \<subseteq> enat ` {.. n})"
         using \<open>infinite X\<close> by (auto dest: finite_subset)
-      then obtain x where "x \<in> X" "x \<notin> enat ` {..n}"
+      then obtain x where x: "x \<in> X" "x \<notin> enat ` {..n}"
         by blast
-      moreover then have "of_nat n \<le> x"
+      then have "of_nat n \<le> x"
         by (cases x) (auto simp: of_nat_eq_enat)
-      ultimately show ?thesis
+      with x show ?thesis
         by (auto intro!: bexI[of _ x] less_le_trans[OF n])
     qed
     then have "(SUP x : X. ennreal_of_enat x) = top"
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -2036,14 +2036,15 @@
 lemma SUP_ereal_add_left:
   assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
   shows "(SUP i:I. f i + c :: ereal) = (SUP i:I. f i) + c"
-proof cases
-  assume "(SUP i:I. f i) = - \<infinity>"
-  moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = -\<infinity>"
+proof (cases "(SUP i:I. f i) = - \<infinity>")
+  case True
+  then have "\<And>i. i \<in> I \<Longrightarrow> f i = -\<infinity>"
     unfolding Sup_eq_MInfty by auto
-  ultimately show ?thesis
+  with True show ?thesis
     by (cases c) (auto simp: \<open>I \<noteq> {}\<close>)
 next
-  assume "(SUP i:I. f i) \<noteq> - \<infinity>" then show ?thesis
+  case False
+  then show ?thesis
     by (subst continuous_at_Sup_mono[where f="\<lambda>x. x + c"])
        (auto simp: continuous_at_imp_continuous_at_within continuous_at mono_def ereal_add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close>)
 qed
@@ -2158,14 +2159,15 @@
   assumes "I \<noteq> {}"
   assumes f: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" and c: "0 \<le> c"
   shows "(SUP i:I. c * f i) = c * (SUP i:I. f i)"
-proof cases
-  assume "(SUP i: I. f i) = 0"
-  moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = 0"
+proof (cases "(SUP i: I. f i) = 0")
+  case True
+  then have "\<And>i. i \<in> I \<Longrightarrow> f i = 0"
     by (metis SUP_upper f antisym)
-  ultimately show ?thesis
+  with True show ?thesis
     by simp
 next
-  assume "(SUP i:I. f i) \<noteq> 0" then show ?thesis
+  case False
+  then show ?thesis
     by (subst continuous_at_Sup_mono[where f="\<lambda>x. c * x"])
        (auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \<open>I \<noteq> {}\<close>
              intro!: ereal_mult_left_mono c)
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Library/Function_Growth.thy
--- a/src/HOL/Library/Function_Growth.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Function_Growth.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -36,8 +36,8 @@
   shows "a ^ (m - n) = (a ^ m) div (a ^ n)"
 proof -
   define q where "q = m - n"
-  moreover with assms have "m = q + n" by (simp add: q_def)
-  ultimately show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
+  with assms have "m = q + n" by (simp add: q_def)
+  with q_def show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
 qed
 
 
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/More_List.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -317,10 +317,10 @@
   then show ?Q
   proof (rule nth_equalityI [rule_format])
     fix n
-    assume "n < length ?xs"
-    moreover with len have "n < length ?ys"
+    assume n: "n < length ?xs"
+    with len have "n < length ?ys"
       by simp
-    ultimately have xs: "nth_default dflt ?xs n = ?xs ! n"
+    with n have xs: "nth_default dflt ?xs n = ?xs ! n"
       and ys: "nth_default dflt ?ys n = ?ys ! n"
       by (simp_all only: nth_default_nth)
     with eq show "?xs ! n = ?ys ! n"
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -2410,11 +2410,11 @@
         moreover have "(a, b) \<in> (r \<inter> D \<times> D)\<inverse>"
           using \<open>(b, a) \<in> r\<close> using \<open>b \<in># B\<close> and \<open>a \<in># B\<close>
           by (auto simp: D_def)
-        ultimately obtain x where "x \<in># X" and "(a, x) \<in> r"
+        ultimately obtain x where x: "x \<in># X" "(a, x) \<in> r"
           using "1.IH" by blast
-        moreover then have "(b, x) \<in> r"
+        then have "(b, x) \<in> r"
           using \<open>trans r\<close> and \<open>(b, a) \<in> r\<close> by (auto dest: transD)
-        ultimately show ?thesis by blast
+        with x show ?thesis by blast
       qed blast
     qed }
   note B_less = this
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Library/Order_Continuity.thy
--- a/src/HOL/Library/Order_Continuity.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Order_Continuity.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -72,10 +72,11 @@
   shows "sup_continuous (\<lambda>x. f (g x))"
   unfolding sup_continuous_def
 proof safe
-  fix M :: "nat \<Rightarrow> 'c" assume "mono M"
-  moreover then have "mono (\<lambda>i. g (M i))"
+  fix M :: "nat \<Rightarrow> 'c"
+  assume M: "mono M"
+  then have "mono (\<lambda>i. g (M i))"
     using sup_continuous_mono[OF g] by (auto simp: mono_def)
-  ultimately show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))"
+  with M show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))"
     by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
 qed
 
@@ -269,10 +270,11 @@
   shows "inf_continuous (\<lambda>x. f (g x))"
   unfolding inf_continuous_def
 proof safe
-  fix M :: "nat \<Rightarrow> 'c" assume "antimono M"
-  moreover then have "antimono (\<lambda>i. g (M i))"
+  fix M :: "nat \<Rightarrow> 'c"
+  assume M: "antimono M"
+  then have "antimono (\<lambda>i. g (M i))"
     using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def)
-  ultimately show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))"
+  with M show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))"
     by (auto simp: inf_continuous_def g[THEN inf_continuousD] f[THEN inf_continuousD])
 qed
 
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Library/Perm.thy
--- a/src/HOL/Library/Perm.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Perm.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -78,15 +78,15 @@
   assume "card (affected f) = 1"
   then obtain a where *: "affected f = {a}"
     by (rule card_1_singletonE)
-  then have "f \<langle>$\<rangle> a \<noteq> a"
+  then have **: "f \<langle>$\<rangle> a \<noteq> a"
     by (simp add: in_affected [symmetric])
-  moreover with * have "f \<langle>$\<rangle> a \<notin> affected f"
+  with * have "f \<langle>$\<rangle> a \<notin> affected f"
     by simp
   then have "f \<langle>$\<rangle> (f \<langle>$\<rangle> a) = f \<langle>$\<rangle> a"
     by (simp add: in_affected)
   then have "inv (apply f) (f \<langle>$\<rangle> (f \<langle>$\<rangle> a)) = inv (apply f) (f \<langle>$\<rangle> a)"
     by simp
-  ultimately show False by simp
+  with ** show False by simp
 qed
 
 
@@ -203,15 +203,18 @@
     using assms by auto
   then show "(g * f) \<langle>$\<rangle> a = (f * g) \<langle>$\<rangle> a"
   proof cases
-    case 1 moreover with * have "f \<langle>$\<rangle> a \<notin> affected g"
+    case 1
+    with * have "f \<langle>$\<rangle> a \<notin> affected g"
       by auto
-    ultimately show ?thesis by (simp add: in_affected apply_times)
+    with 1 show ?thesis by (simp add: in_affected apply_times)
   next
-    case 2 moreover with * have "g \<langle>$\<rangle> a \<notin> affected f"
+    case 2
+    with * have "g \<langle>$\<rangle> a \<notin> affected f"
       by auto
-    ultimately show ?thesis by (simp add: in_affected apply_times)
+    with 2 show ?thesis by (simp add: in_affected apply_times)
   next
-    case 3 then show ?thesis by (simp add: in_affected apply_times)
+    case 3
+    then show ?thesis by (simp add: in_affected apply_times)
   qed
 qed
 
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/List.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -3542,10 +3542,9 @@
 
     have "length ys = card (f ` {0 ..< size [x]})"
       using f_img by auto
-    then have "length ys = 1" by auto
-    moreover
+    then have *: "length ys = 1" by auto
     then have "f 0 = 0" using f_img by auto
-    ultimately show ?case using f_nth by (cases ys) auto
+    with * show ?case using f_nth by (cases ys) auto
   next
     case (3 x1 x2 xs)
     from "3.prems" obtain f where f_mono: "mono f"
@@ -5499,10 +5498,10 @@
   next
     let ?k = "length abs"
     case eq
-    hence "abs = bcs" "b = b'" using bs bs' by auto
-    moreover hence "(a, c') \<in> r"
+    hence *: "abs = bcs" "b = b'" using bs bs' by auto
+    hence "(a, c') \<in> r"
       using abr b'c'r assms unfolding trans_def by blast
-    ultimately show ?thesis using n n' unfolding lexn_conv as bs cs by auto
+    with * show ?thesis using n n' unfolding lexn_conv as bs cs by auto
   qed
 qed
 
@@ -5840,8 +5839,8 @@
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?lhs
-  moreover hence "\<not> lexordp_eq ys xs" by induct simp_all
-  ultimately show ?rhs by(simp add: lexordp_into_lexordp_eq)
+  hence "\<not> lexordp_eq ys xs" by induct simp_all
+  with \<open>?lhs\<close> show ?rhs by (simp add: lexordp_into_lexordp_eq)
 next
   assume ?rhs
   hence "lexordp_eq xs ys" "\<not> lexordp_eq ys xs" by simp_all
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -71,9 +71,9 @@
 proof (induct s rule: finite_ne_induct)
   case (insert b s)
   assume *: "\<forall>x\<in>insert b s. \<forall>y\<in>insert b s. x \<le> y \<or> y \<le> x"
-  moreover then obtain u l where "l \<in> s" "\<forall>b\<in>s. l \<le> b" "u \<in> s" "\<forall>b\<in>s. b \<le> u"
+  then obtain u l where "l \<in> s" "\<forall>b\<in>s. l \<le> b" "u \<in> s" "\<forall>b\<in>s. b \<le> u"
     using insert by auto
-  ultimately show "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. a \<le> x" "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. x \<le> a"
+  with * show "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. a \<le> x" "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. x \<le> a"
     using *[rule_format, of b u] *[rule_format, of b l] by (metis insert_iff order.trans)+
 qed auto
 
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Multivariate_Analysis/Conformal_Mappings.thy
--- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -1411,7 +1411,7 @@
   show no_df0: "norm(deriv f 0) \<le> 1"
     by (simp add: \<open>\<And>z. cmod z < 1 \<Longrightarrow> cmod (h z) \<le> 1\<close> df0)
   show "?Q" if "?P"
-  using that
+    using that
   proof
     assume "\<exists>z. cmod z < 1 \<and> z \<noteq> 0 \<and> cmod (f z) = cmod z"
     then obtain \<gamma> where \<gamma>: "cmod \<gamma> < 1" "\<gamma> \<noteq> 0" "cmod (f \<gamma>) = cmod \<gamma>" by blast
@@ -1424,9 +1424,9 @@
       by (metis add_diff_cancel_left' diff_diff_eq2 le_less_trans noh_le norm_triangle_ineq4)
     ultimately obtain c where c: "\<And>z. norm z < 1 \<Longrightarrow> h z = c"
       using Schwarz2 [OF holh, of "1 - norm \<gamma>" \<gamma>, unfolded constant_on_def] \<gamma> by auto
-    moreover then have "norm c = 1"
+    then have "norm c = 1"
       using \<gamma> by force
-    ultimately show ?thesis
+    with c show ?thesis
       using fz_eq by auto
   next
     assume [simp]: "cmod (deriv f 0) = 1"
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -10168,14 +10168,14 @@
   then have x: "{integral s (f k) |k. True} = range x"
     by auto
 
-  have "g integrable_on s \<and> (\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
+  have *: "g integrable_on s \<and> (\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
   proof (intro monotone_convergence_increasing allI ballI assms)
     show "bounded {integral s (f k) |k. True}"
       unfolding x by (rule convergent_imp_bounded) fact
   qed (auto intro: f)
-  moreover then have "integral s g = x'"
+  then have "integral s g = x'"
     by (intro LIMSEQ_unique[OF _ \<open>x \<longlonglongrightarrow> x'\<close>]) (simp add: x_eq)
-  ultimately show ?thesis
+  with * show ?thesis
     by (simp add: has_integral_integral)
 qed
 
@@ -11559,18 +11559,16 @@
     with \<open>open W\<close>
     have "\<exists>X0 Y. open X0 \<and> open Y \<and> x0 \<in> X0 \<and> y \<in> Y \<and> X0 \<times> Y \<subseteq> W"
       by (rule open_prod_elim) blast
-  } then obtain X0 Y where
-    "\<forall>y \<in> K. open (X0 y) \<and> open (Y y) \<and> x0 \<in> X0 y \<and> y \<in> Y y \<and> X0 y \<times> Y y \<subseteq> W"
+  }
+  then obtain X0 Y where
+    *: "\<forall>y \<in> K. open (X0 y) \<and> open (Y y) \<and> x0 \<in> X0 y \<and> y \<in> Y y \<and> X0 y \<times> Y y \<subseteq> W"
     by metis
-  moreover
-  then have "\<forall>t\<in>Y ` K. open t" "K \<subseteq> \<Union>(Y ` K)" by auto
-  with \<open>compact K\<close> obtain CC where "CC \<subseteq> Y ` K" "finite CC" "K \<subseteq> \<Union>CC"
+  from * have "\<forall>t\<in>Y ` K. open t" "K \<subseteq> \<Union>(Y ` K)" by auto
+  with \<open>compact K\<close> obtain CC where CC: "CC \<subseteq> Y ` K" "finite CC" "K \<subseteq> \<Union>CC"
     by (rule compactE)
-  moreover
-  then obtain c where c:
-    "\<And>C. C \<in> CC \<Longrightarrow> c C \<in> K \<and> C = Y (c C)"
+  then obtain c where c: "\<And>C. C \<in> CC \<Longrightarrow> c C \<in> K \<and> C = Y (c C)"
     by (force intro!: choice)
-  ultimately show ?thesis
+  with * CC show ?thesis
     by (force intro!: exI[where x="\<Inter>C\<in>CC. X0 (c C)"])
 qed
 
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -3057,11 +3057,11 @@
     then have ftendsw: "((\<lambda>n. f (z n)) \<circ> K) \<longlonglongrightarrow> w"
       by (metis LIMSEQ_subseq_LIMSEQ fun.map_cong0 fz tendsw)
     have zKs: "\<And>n. (z o K) n \<in> S" by (simp add: zs)
-    have "f \<circ> z = \<xi>"  "(\<lambda>n. f (z n)) = \<xi>"
+    have fz: "f \<circ> z = \<xi>"  "(\<lambda>n. f (z n)) = \<xi>"
       using fz by auto
-    moreover then have "(\<xi> \<circ> K) \<longlonglongrightarrow> f y"
+    then have "(\<xi> \<circ> K) \<longlonglongrightarrow> f y"
       by (metis (no_types) Klim zKs y contf comp_assoc continuous_on_closure_sequentially)
-    ultimately have wy: "w = f y" using fz LIMSEQ_unique ftendsw by auto
+    with fz have wy: "w = f y" using fz LIMSEQ_unique ftendsw by auto
     have rle: "r \<le> norm (f y - f a)"
       apply (rule le_no)
       using w wy oint
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -4343,10 +4343,11 @@
   have "F \<noteq> bot"
     unfolding F_def
   proof (rule INF_filter_not_bot)
-    fix X assume "X \<subseteq> insert U A" "finite X"
-    moreover with A(2)[THEN spec, of "X - {U}"] have "U \<inter> \<Inter>(X - {U}) \<noteq> {}"
+    fix X
+    assume X: "X \<subseteq> insert U A" "finite X"
+    with A(2)[THEN spec, of "X - {U}"] have "U \<inter> \<Inter>(X - {U}) \<noteq> {}"
       by auto
-    ultimately show "(INF a:X. principal a) \<noteq> bot"
+    with X show "(INF a:X. principal a) \<noteq> bot"
       by (auto simp add: INF_principal_finite principal_eq_bot_iff)
   qed
   moreover
@@ -6601,13 +6602,12 @@
       then obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
         by (auto simp: closure_sequential)
       from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y
-      have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x"
+      have hx: "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x"
         by (auto simp: set_mp extension)
-      moreover
       then have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x"
         using \<open>x \<notin> X\<close> not_eventuallyD xs(2)
         by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at xs)
-      ultimately have "h x = y x" by (rule LIMSEQ_unique)
+      with hx have "h x = y x" by (rule LIMSEQ_unique)
     } then
     have "h x = ?g x"
       using extension by auto
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Probability/Distributions.thy
--- a/src/HOL/Probability/Distributions.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Distributions.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -164,8 +164,8 @@
 lemma nn_integral_erlang_density:
   assumes [arith]: "0 < l"
   shows "(\<integral>\<^sup>+ x. ennreal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = erlang_CDF k l a"
-proof cases
-  assume [arith]: "0 \<le> a"
+proof (cases "0 \<le> a")
+  case [arith]: True
   have eq: "\<And>x. indicator {0..a} (x / l) = indicator {0..a*l} x"
     by (simp add: field_simps split: split_indicator)
   have "(\<integral>\<^sup>+x. ennreal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) =
@@ -182,10 +182,10 @@
     by (auto simp: erlang_CDF_def)
   finally show ?thesis .
 next
-  assume "\<not> 0 \<le> a"
-  moreover then have "(\<integral>\<^sup>+ x. ennreal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = (\<integral>\<^sup>+x. 0 \<partial>(lborel::real measure))"
+  case False
+  then have "(\<integral>\<^sup>+ x. ennreal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = (\<integral>\<^sup>+x. 0 \<partial>(lborel::real measure))"
     by (intro nn_integral_cong) (auto simp: erlang_density_def)
-  ultimately show ?thesis
+  with False show ?thesis
     by (simp add: erlang_CDF_def)
 qed
 
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -1133,10 +1133,10 @@
 lemma (in product_sigma_finite) distr_component:
   "distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^sub>M {i} M" (is "?D = ?P")
 proof (intro PiM_eqI)
-  fix A assume "\<And>ia. ia \<in> {i} \<Longrightarrow> A ia \<in> sets (M ia)"
-  moreover then have "(\<lambda>x. \<lambda>i\<in>{i}. x) -` Pi\<^sub>E {i} A \<inter> space (M i) = A i"
+  fix A assume A: "\<And>ia. ia \<in> {i} \<Longrightarrow> A ia \<in> sets (M ia)"
+  then have "(\<lambda>x. \<lambda>i\<in>{i}. x) -` Pi\<^sub>E {i} A \<inter> space (M i) = A i"
     by (auto dest: sets.sets_into_space)
-  ultimately show "emeasure (distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x)) (Pi\<^sub>E {i} A) = (\<Prod>i\<in>{i}. emeasure (M i) (A i))"
+  with A show "emeasure (distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x)) (Pi\<^sub>E {i} A) = (\<Prod>i\<in>{i}. emeasure (M i) (A i))"
     by (subst emeasure_distr) (auto intro!: sets_PiM_I_finite measurable_restrict)
 qed simp_all
 
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -272,28 +272,28 @@
   ultimately show ?case by simp
 next
   case (set B)
-  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B"
+  then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B"
     by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra)
-  ultimately show ?case
+  with set show ?case
     by (simp add: measurable_emeasure_subprob_algebra)
 next
   case (mult f c)
-  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. c * f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. c * \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B"
+  then have "(\<lambda>M'. \<integral>\<^sup>+M''. c * f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. c * \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B"
     by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)
-  ultimately show ?case
+  with mult show ?case
     by simp
 next
   case (add f g)
-  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' + g M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+M''. f M'' \<partial>M') + (\<integral>\<^sup>+M''. g M'' \<partial>M')) \<in> ?B"
+  then have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' + g M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+M''. f M'' \<partial>M') + (\<integral>\<^sup>+M''. g M'' \<partial>M')) \<in> ?B"
     by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra)
-  ultimately show ?case
+  with add show ?case
     by (simp add: ac_simps)
 next
   case (seq F)
-  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. (SUP i. F i) M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. SUP i. (\<integral>\<^sup>+M''. F i M'' \<partial>M')) \<in> ?B"
+  then have "(\<lambda>M'. \<integral>\<^sup>+M''. (SUP i. F i) M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. SUP i. (\<integral>\<^sup>+M''. F i M'' \<partial>M')) \<in> ?B"
     unfolding SUP_apply
     by (intro measurable_cong nn_integral_monotone_convergence_SUP) (auto simp add: space_subprob_algebra)
-  ultimately show ?case
+  with seq show ?case
     by (simp add: ac_simps)
 qed
 
@@ -793,10 +793,10 @@
     by simp
 next
   case (set A)
-  moreover with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)"
+  with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)"
     by (intro nn_integral_cong nn_integral_indicator)
        (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
-  ultimately show ?case
+  with set show ?case
     using M by (simp add: emeasure_join)
 next
   case (mult f c)
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -29,14 +29,18 @@
   note * = this
 
   have "emeasure (PiM I M) (emb I J (PiE J X)) = (\<Prod>i\<in>J. M i (X i))"
-  proof cases
-    assume "\<not> (J \<noteq> {} \<or> I = {})"
-    then obtain i where "J = {}" "i \<in> I" by auto
-    moreover then have "emb I {} {\<lambda>x. undefined} = emb I {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i))"
+  proof (cases "J \<noteq> {} \<or> I = {}")
+    case False
+    then obtain i where i: "J = {}" "i \<in> I" by auto
+    then have "emb I {} {\<lambda>x. undefined} = emb I {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i))"
       by (auto simp: space_PiM prod_emb_def)
-    ultimately show ?thesis
+    with i show ?thesis
       by (simp add: * M.emeasure_space_1)
-  qed (simp add: *[OF _ assms X])
+  next
+    case True
+    then show ?thesis
+      by (simp add: *[OF _ assms X])
+  qed
   with assms show "emeasure (distr (Pi\<^sub>M I M) (Pi\<^sub>M J M) (\<lambda>x. restrict x J)) (Pi\<^sub>E J X) = (\<Prod>i\<in>J. emeasure (M i) (X i))"
     by (subst emeasure_distr_restrict[OF _ refl]) (auto intro!: sets_PiM_I_finite X)
 qed (insert assms, auto)
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Probability/Lebesgue_Integral_Substitution.thy
--- a/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -323,9 +323,9 @@
     and "(LBINT x. f x * indicator {g a..g b} x) = (LBINT x. f (g x) * g' x * indicator {a..b} x)"
 proof-
   from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
-  from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and
-                             Mg': "set_borel_measurable borel {a..b} g'"
-      by (simp_all only: set_measurable_continuous_on_ivl)
+  with contg' have Mg: "set_borel_measurable borel {a..b} g"
+    and Mg': "set_borel_measurable borel {a..b} g'"
+    by (simp_all only: set_measurable_continuous_on_ivl)
   from derivg derivg_nonneg have monog: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
     by (rule deriv_nonneg_imp_mono) simp_all
 
@@ -341,18 +341,18 @@
           enn2real (\<integral>\<^sup>+ x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) -
           enn2real (\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel)" using integrable
     by (subst real_lebesgue_integral_def) (simp_all add: nn_integral_set_ennreal mult.commute)
-  also have "(\<integral>\<^sup>+x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) =
-               (\<integral>\<^sup>+x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel)"
+  also have *: "(\<integral>\<^sup>+x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) =
+      (\<integral>\<^sup>+x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel)"
     by (intro nn_integral_cong) (simp split: split_indicator)
-  also with M1 have A: "(\<integral>\<^sup>+ x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel) =
+  also from M1 * have A: "(\<integral>\<^sup>+ x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel) =
                             (\<integral>\<^sup>+ x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel)"
     by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \<open>a \<le> b\<close>])
        (auto simp: nn_integral_set_ennreal mult.commute)
-  also have "(\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel) =
-               (\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel)"
+  also have **: "(\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel) =
+      (\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel)"
     by (intro nn_integral_cong) (simp split: split_indicator)
-  also with M2 have B: "(\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel) =
-                            (\<integral>\<^sup>+ x. ennreal (- (f (g x)) * g' x * indicator {a..b} x) \<partial>lborel)"
+  also from M2 ** have B: "(\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel) =
+        (\<integral>\<^sup>+ x. ennreal (- (f (g x)) * g' x * indicator {a..b} x) \<partial>lborel)"
     by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \<open>a \<le> b\<close>])
        (auto simp: nn_integral_set_ennreal mult.commute)
 
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -75,9 +75,9 @@
           fix i assume "i \<in> S - {m}"
           then have i: "i \<in> S" "i \<noteq> m" by auto
           { assume i': "l i < r i" "l i < r m"
-            moreover with \<open>finite S\<close> i m have "l m \<le> l i"
+            with \<open>finite S\<close> i m have "l m \<le> l i"
               by auto
-            ultimately have "{l i <.. r i} \<inter> {l m <.. r m} \<noteq> {}"
+            with i' have "{l i <.. r i} \<inter> {l m <.. r m} \<noteq> {}"
               by auto
             then have False
               using disjoint_family_onD[OF disj, of i m] i by auto }
@@ -852,9 +852,9 @@
   shows "(f has_integral r) UNIV"
 using f proof (induct f arbitrary: r rule: borel_measurable_induct_real)
   case (set A)
-  moreover then have "((\<lambda>x. 1) has_integral measure lborel A) A"
+  then have "((\<lambda>x. 1) has_integral measure lborel A) A"
     by (intro has_integral_measure_lborel) (auto simp: ennreal_indicator)
-  ultimately show ?case
+  with set show ?case
     by (simp add: ennreal_indicator measure_def) (simp add: indicator_def)
 next
   case (mult g c)
@@ -868,13 +868,12 @@
     by (auto intro!: has_integral_cmult_real)
 next
   case (add g h)
-  moreover
   then have "(\<integral>\<^sup>+ x. h x + g x \<partial>lborel) = (\<integral>\<^sup>+ x. h x \<partial>lborel) + (\<integral>\<^sup>+ x. g x \<partial>lborel)"
     by (simp add: nn_integral_add)
   with add obtain a b where "0 \<le> a" "0 \<le> b" "(\<integral>\<^sup>+ x. h x \<partial>lborel) = ennreal a" "(\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal b" "r = a + b"
     by (cases "\<integral>\<^sup>+ x. h x \<partial>lborel" "\<integral>\<^sup>+ x. g x \<partial>lborel" rule: ennreal2_cases)
        (auto simp: add_top nn_integral_add top_add ennreal_plus[symmetric] simp del: ennreal_plus)
-  ultimately show ?case
+  with add show ?case
     by (auto intro!: has_integral_add)
 next
   case (seq U)
@@ -1020,8 +1019,8 @@
   fixes A :: "'a::euclidean_space set"
   assumes A[measurable]: "A \<in> sets borel" and [simp]: "0 \<le> r"
   shows "((\<lambda>x. 1) has_integral r) A \<longleftrightarrow> emeasure lborel A = ennreal r"
-proof cases
-  assume emeasure_A: "emeasure lborel A = \<infinity>"
+proof (cases "emeasure lborel A = \<infinity>")
+  case emeasure_A: True
   have "\<not> (\<lambda>x. 1::real) integrable_on A"
   proof
     assume int: "(\<lambda>x. 1::real) integrable_on A"
@@ -1035,10 +1034,10 @@
   with emeasure_A show ?thesis
     by auto
 next
-  assume "emeasure lborel A \<noteq> \<infinity>"
-  moreover then have "((\<lambda>x. 1) has_integral measure lborel A) A"
+  case False
+  then have "((\<lambda>x. 1) has_integral measure lborel A) A"
     by (simp add: has_integral_measure_lborel less_top)
-  ultimately show ?thesis
+  with False show ?thesis
     by (auto simp: emeasure_eq_ennreal_measure has_integral_unique)
 qed
 
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Probability/Levy.thy
--- a/src/HOL/Probability/Levy.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Levy.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -391,23 +391,22 @@
                 continuous_intros ballI M'.isCont_char continuous_intros)
     have "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> LBINT t:{-d/2..d/2}. cmod (1 - char M' t)"
       using integral_norm_bound[OF 2] by simp
-    also have "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4"
+    also have 4: "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4"
       apply (rule integral_mono [OF 3])
-      apply (simp add: emeasure_lborel_Icc_eq)
-      apply (case_tac "x \<in> {-d/2..d/2}", auto)
+       apply (simp add: emeasure_lborel_Icc_eq)
+      apply (case_tac "x \<in> {-d/2..d/2}")
+       apply auto
       apply (subst norm_minus_commute)
       apply (rule less_imp_le)
       apply (rule d1 [simplified])
-      using d0 by auto
-    also with d0 have "\<dots> = d * \<epsilon> / 4"
+      using d0 apply auto
+      done
+    also from d0 4 have "\<dots> = d * \<epsilon> / 4"
       by simp
     finally have bound: "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> d * \<epsilon> / 4" .
-    { fix n x
-      have "cmod (1 - char (M n) x) \<le> 2"
-        by (rule order_trans [OF norm_triangle_ineq4], auto simp add: Mn.cmod_char_le_1)
-    } note bd1 = this
-    have "(\<lambda>n. CLBINT t:{-d/2..d/2}. 1 - char (M n) t) \<longlonglongrightarrow> (CLBINT t:{-d/2..d/2}. 1 - char M' t)"
-      using bd1
+    have "cmod (1 - char (M n) x) \<le> 2" for n x
+      by (rule order_trans [OF norm_triangle_ineq4], auto simp add: Mn.cmod_char_le_1)
+    then have "(\<lambda>n. CLBINT t:{-d/2..d/2}. 1 - char (M n) t) \<longlonglongrightarrow> (CLBINT t:{-d/2..d/2}. 1 - char M' t)"
       apply (intro integral_dominated_convergence[where w="\<lambda>x. indicator {-d/2..d/2} x *\<^sub>R 2"])
       apply (auto intro!: char_conv tendsto_intros
                   simp: emeasure_lborel_Icc_eq
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -1862,7 +1862,7 @@
     using f unfolding Pi_def bij_betw_def by auto
   fix X assume "X \<in> sets (distr (count_space A) (count_space B) f)"
   then have X: "X \<in> sets (count_space B)" by auto
-  moreover then have "f -` X \<inter> A = the_inv_into A f ` X"
+  moreover from X have "f -` X \<inter> A = the_inv_into A f ` X"
     using f by (auto simp: bij_betw_def subset_image_iff image_iff the_inv_into_f_f intro: the_inv_into_f_f[symmetric])
   moreover have "inj_on (the_inv_into A f) B"
     using X f by (auto simp: bij_betw_def inj_on_the_inv_into)
@@ -1932,8 +1932,8 @@
 lemma emeasure_restrict_space:
   assumes "\<Omega> \<inter> space M \<in> sets M" "A \<subseteq> \<Omega>"
   shows "emeasure (restrict_space M \<Omega>) A = emeasure M A"
-proof cases
-  assume "A \<in> sets M"
+proof (cases "A \<in> sets M")
+  case True
   show ?thesis
   proof (rule emeasure_measure_of[OF restrict_space_def])
     show "op \<inter> \<Omega> ` sets M \<subseteq> Pow (\<Omega> \<inter> space M)" "A \<in> sets (restrict_space M \<Omega>)"
@@ -1951,10 +1951,10 @@
     qed
   qed
 next
-  assume "A \<notin> sets M"
-  moreover with assms have "A \<notin> sets (restrict_space M \<Omega>)"
+  case False
+  with assms have "A \<notin> sets (restrict_space M \<Omega>)"
     by (simp add: sets_restrict_space_iff)
-  ultimately show ?thesis
+  with False show ?thesis
     by (simp add: emeasure_notin_sets)
 qed
 
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -1734,7 +1734,7 @@
 proof (rule measure_eqI)
   fix X assume "X \<in> sets M"
   then have X: "X \<subseteq> A" by auto
-  moreover with A have "countable X" by (auto dest: countable_subset)
+  moreover from A X have "countable X" by (auto dest: countable_subset)
   ultimately have
     "emeasure M X = (\<integral>\<^sup>+a. emeasure M {a} \<partial>count_space X)"
     "emeasure N X = (\<integral>\<^sup>+a. emeasure N {a} \<partial>count_space X)"
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -1104,17 +1104,17 @@
   assume eq: "\<forall>x\<in>set_pmf p. \<forall>y\<in>set_pmf q. R x y \<longrightarrow> measure p {x. R x y} = measure q {y. R x y}"
 
   show "measure p C = measure q C"
-  proof cases
-    assume "p \<inter> C = {}"
-    moreover then have "q \<inter> C = {}"
+  proof (cases "p \<inter> C = {}")
+    case True
+    then have "q \<inter> C = {}"
       using quotient_rel_set_disjoint[OF assms C R] by simp
-    ultimately show ?thesis
+    with True show ?thesis
       unfolding measure_pmf_zero_iff[symmetric] by simp
   next
-    assume "p \<inter> C \<noteq> {}"
-    moreover then have "q \<inter> C \<noteq> {}"
+    case False
+    then have "q \<inter> C \<noteq> {}"
       using quotient_rel_set_disjoint[OF assms C R] by simp
-    ultimately obtain x y where in_set: "x \<in> set_pmf p" "y \<in> set_pmf q" and in_C: "x \<in> C" "y \<in> C"
+    with False obtain x y where in_set: "x \<in> set_pmf p" "y \<in> set_pmf q" and in_C: "x \<in> C" "y \<in> C"
       by auto
     then have "R x y"
       using in_quotient_imp_in_rel[of UNIV ?R C x y] C assms
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -840,11 +840,11 @@
   assumes "f \<in> borel_measurable M" "density M f = N"
   shows "density M (RN_deriv M N) = N"
 proof -
-  have "\<exists>f. f \<in> borel_measurable M \<and> density M f = N"
+  have *: "\<exists>f. f \<in> borel_measurable M \<and> density M f = N"
     using assms by auto
-  moreover then have "density M (SOME f. f \<in> borel_measurable M \<and> density M f = N) = N"
+  then have "density M (SOME f. f \<in> borel_measurable M \<and> density M f = N) = N"
     by (rule someI2_ex) auto
-  ultimately show ?thesis
+  with * show ?thesis
     by (auto simp: RN_deriv_def)
 qed
 
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Probability/SPMF.thy
--- a/src/HOL/Probability/SPMF.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/SPMF.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -2520,8 +2520,8 @@
     ultimately have "(weight_spmf p * weight_spmf q) * (weight_spmf p * weight_spmf q) = 1" by simp
     hence *: "weight_spmf p * weight_spmf q = 1"
       by(metis antisym_conv less_le mult_less_cancel_left1 weight_pair_spmf weight_spmf_le_1 weight_spmf_nonneg)
-    hence "weight_spmf p = 1" by(metis antisym_conv mult_left_le weight_spmf_le_1 weight_spmf_nonneg)
-    moreover with * have "weight_spmf q = 1" by simp
+    hence **: "weight_spmf p = 1" by(metis antisym_conv mult_left_le weight_spmf_le_1 weight_spmf_nonneg)
+    moreover from * ** have "weight_spmf q = 1" by simp
     moreover note calculation }
   note full = this
 
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Quotient_Examples/Int_Pow.thy
--- a/src/HOL/Quotient_Examples/Int_Pow.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Quotient_Examples/Int_Pow.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -41,8 +41,8 @@
   "[| x \<in> Units G; y \<in> Units G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
 proof -
   assume G: "x \<in> Units G"  "y \<in> Units G"
-  moreover then have "x \<in> carrier G"  "y \<in> carrier G" by auto
-  ultimately have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
+  then have "x \<in> carrier G"  "y \<in> carrier G" by auto
+  with G have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
     by (simp add: m_assoc) (simp add: m_assoc [symmetric])
   with G show ?thesis by (simp del: Units_l_inv)
 qed
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Set_Interval.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -578,9 +578,9 @@
   obtain y where "Max {a <..} < y"
     using gt_ex by auto
 
-  obtain x where "a < x"
+  obtain x where x: "a < x"
     using gt_ex by auto
-  also then have "x \<le> Max {a <..}"
+  also from x have "x \<le> Max {a <..}"
     by fact
   also note \<open>Max {a <..} < y\<close>
   finally have "y \<le> Max { a <..}"
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Transcendental.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -1617,14 +1617,15 @@
 
 lemma isCont_ln:
   fixes x::real assumes "x \<noteq> 0" shows "isCont ln x"
-proof cases
-  assume "0 < x"
-  moreover then have "isCont ln (exp (ln x))"
+proof (cases "0 < x")
+  case True
+  then have "isCont ln (exp (ln x))"
     by (intro isCont_inv_fun[where d="\<bar>x\<bar>" and f=exp]) auto
-  ultimately show ?thesis
+  with True show ?thesis
     by simp
 next
-  assume "\<not> 0 < x" with \<open>x \<noteq> 0\<close> show "isCont ln x"
+  case False
+  with \<open>x \<noteq> 0\<close> show "isCont ln x"
     unfolding isCont_def
     by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\<lambda>_. ln 0"])
        (auto simp: ln_neg_is_const not_less eventually_at dist_real_def
@@ -4902,11 +4903,11 @@
   have x1: "x \<le> 1"
     using assms
     by (metis le_add_same_cancel1 power2_le_imp_le power_one zero_le_power2)
-  moreover with assms have ax: "0 \<le> arccos x" "cos(arccos x) = x"
+  with assms have ax: "0 \<le> arccos x" "cos (arccos x) = x"
     by (auto simp: arccos)
-  moreover have "y = sqrt (1 - x\<^sup>2)" using assms
+  from assms have "y = sqrt (1 - x\<^sup>2)"
     by (metis abs_of_nonneg add.commute add_diff_cancel real_sqrt_abs)
-  ultimately show ?thesis using assms arccos_le_pi2 [of x]
+  with x1 ax assms arccos_le_pi2 [of x] show ?thesis
     by (rule_tac x="arccos x" in exI) (auto simp: sin_arccos)
 qed
 
@@ -5836,26 +5837,25 @@
     assume ?lhs
     with * have "(\<forall>i\<le>n. c i = (if i=0 then k else 0))"
       by (simp add: polyfun_eq_coeffs [symmetric])
-    then show ?rhs
-      by simp
+    then show ?rhs by simp
   next
-    assume ?rhs then show ?lhs
-      by (induct n) auto
+    assume ?rhs
+    then show ?lhs by (induct n) auto
   qed
 qed
 
 lemma root_polyfun:
-  fixes z:: "'a::idom"
+  fixes z :: "'a::idom"
   assumes "1 \<le> n"
-    shows "z^n = a \<longleftrightarrow> (\<Sum>i\<le>n. (if i = 0 then -a else if i=n then 1 else 0) * z^i) = 0"
+  shows "z^n = a \<longleftrightarrow> (\<Sum>i\<le>n. (if i = 0 then -a else if i=n then 1 else 0) * z^i) = 0"
   using assms
-  by (cases n; simp add: setsum_head_Suc atLeast0AtMost [symmetric])
+  by (cases n) (simp_all add: setsum_head_Suc atLeast0AtMost [symmetric])
 
 lemma
-    fixes zz :: "'a::{idom,real_normed_div_algebra}"
+  fixes zz :: "'a::{idom,real_normed_div_algebra}"
   assumes "1 \<le> n"
-    shows finite_roots_unity: "finite {z::'a. z^n = 1}"
-      and card_roots_unity:   "card {z::'a. z^n = 1} \<le> n"
+  shows finite_roots_unity: "finite {z::'a. z^n = 1}"
+    and card_roots_unity: "card {z::'a. z^n = 1} \<le> n"
   using polyfun_rootbound [of "\<lambda>i. if i = 0 then -1 else if i=n then 1 else 0" n n] assms
   by (auto simp add: root_polyfun [OF assms])
 
diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/ex/Ballot.thy
--- a/src/HOL/ex/Ballot.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/ex/Ballot.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -180,10 +180,10 @@
       by auto
     show "(\<lambda>V. V - {?l}) \<in> ?V (\<lambda>V. ?l \<in> V) \<rightarrow> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> ?Q V (a + Suc b)}"
       by (auto simp: Ico_subset_finite *)
-    { fix V assume "V \<subseteq> {0..<?l}"
-      moreover then have "finite V" "?l \<notin> V" "{0..<Suc ?l} \<inter> V = V"
+    { fix V assume V: "V \<subseteq> {0..<?l}"
+      then have "finite V" "?l \<notin> V" "{0..<Suc ?l} \<inter> V = V"
         by (auto dest: finite_subset)
-      ultimately have "card (insert ?l V) = Suc (card V)"
+      with V have "card (insert ?l V) = Suc (card V)"
         "card ({0..<m} \<inter> insert ?l V) = (if m = Suc ?l then Suc (card V) else card ({0..<m} \<inter> V))"
         if "m \<le> Suc ?l" for m
         using that by auto }