# HG changeset patch
# User wenzelm
# Date 1470833459 -7200
# Node ID e690d6f2185b3b7e1c34445fd7e9127b02198ce1
# Parent  f9f3006a5579b2b686eaa1b2f0f2979c13aacad8
tuned proofs;

diff -r f9f3006a5579 -r e690d6f2185b src/HOL/Library/AList_Mapping.thy
--- a/src/HOL/Library/AList_Mapping.thy	Wed Aug 10 09:33:54 2016 +0200
+++ b/src/HOL/Library/AList_Mapping.thy	Wed Aug 10 14:50:59 2016 +0200
@@ -22,7 +22,7 @@
   by transfer simp
 
 lemma is_empty_Mapping [code]: "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
-  by (case_tac xs) (simp_all add: is_empty_def null_def)
+  by (cases xs) (simp_all add: is_empty_def null_def)
 
 lemma update_Mapping [code]: "Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)"
   by transfer (simp add: update_conv')
diff -r f9f3006a5579 -r e690d6f2185b src/HOL/Library/Complete_Partial_Order2.thy
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Wed Aug 10 09:33:54 2016 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Wed Aug 10 14:50:59 2016 +0200
@@ -58,11 +58,17 @@
 lemma Sup_minus_bot: 
   assumes chain: "Complete_Partial_Order.chain op \<le> A"
   shows "\<Squnion>(A - {\<Squnion>{}}) = \<Squnion>A"
-apply(rule antisym)
- apply(blast intro: ccpo_Sup_least chain_Diff[OF chain] ccpo_Sup_upper[OF chain])
-apply(rule ccpo_Sup_least[OF chain])
-apply(case_tac "x = \<Squnion>{}")
-by(blast intro: ccpo_Sup_least chain_empty ccpo_Sup_upper[OF chain_Diff[OF chain]])+
+    (is "?lhs = ?rhs")
+proof (rule antisym)
+  show "?lhs \<le> ?rhs"
+    by (blast intro: ccpo_Sup_least chain_Diff[OF chain] ccpo_Sup_upper[OF chain])
+  show "?rhs \<le> ?lhs"
+  proof (rule ccpo_Sup_least [OF chain])
+    show "x \<in> A \<Longrightarrow> x \<le> ?lhs" for x
+      by (cases "x = \<Squnion>{}")
+        (blast intro: ccpo_Sup_least chain_empty ccpo_Sup_upper[OF chain_Diff[OF chain]])+
+  qed
+qed
 
 lemma mono_lub:
   fixes le_b (infix "\<sqsubseteq>" 60)
diff -r f9f3006a5579 -r e690d6f2185b src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Wed Aug 10 09:33:54 2016 +0200
+++ b/src/HOL/Library/Convex.thy	Wed Aug 10 14:50:59 2016 +0200
@@ -287,18 +287,20 @@
   assumes "finite s"
   shows "convex s \<longleftrightarrow> (\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) s \<in> s)"
   unfolding convex_explicit
-proof safe
-  fix t u
-  assume sum: "\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> s"
-    and as: "finite t" "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = (1::real)"
-  have *: "s \<inter> t = t"
-    using as(2) by auto
-  have if_distrib_arg: "\<And>P f g x. (if P then f else g) x = (if P then f x else g x)"
-    by simp
-  show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
-    using sum[THEN spec[where x="\<lambda>x. if x\<in>t then u x else 0"]] as *
-    by (auto simp: assms setsum.If_cases if_distrib if_distrib_arg)
-qed (erule_tac x=s in allE, erule_tac x=u in allE, auto)
+  apply safe
+  subgoal for u by (erule allE [where x=s], erule allE [where x=u]) auto
+  subgoal for t u
+  proof -
+    have if_distrib_arg: "\<And>P f g x. (if P then f else g) x = (if P then f x else g x)"
+      by simp
+    assume sum: "\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> s"
+    assume *: "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1"
+    assume "t \<subseteq> s"
+    then have "s \<inter> t = t" by auto
+    with sum[THEN spec[where x="\<lambda>x. if x\<in>t then u x else 0"]] * show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
+      by (auto simp: assms setsum.If_cases if_distrib if_distrib_arg)
+  qed
+  done 
 
 
 subsection \<open>Functions that are convex on a set\<close>
diff -r f9f3006a5579 -r e690d6f2185b src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Wed Aug 10 09:33:54 2016 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Wed Aug 10 14:50:59 2016 +0200
@@ -304,10 +304,9 @@
    (is "?lhs = ?rhs")
 proof
   assume ?lhs
-  then show ?rhs
-    apply (rule_tac x="inv_into A f ` B" in exI)
-    apply (auto simp: f_inv_into_f subset_iff image_inv_into_cancel inv_into_into)
-    done
+  show ?rhs
+    by (rule exI [where x="inv_into A f ` B"])
+      (use \<open>?lhs\<close> in \<open>auto simp: f_inv_into_f subset_iff image_inv_into_cancel inv_into_into\<close>)
 next
   assume ?rhs
   then show ?lhs by force
diff -r f9f3006a5579 -r e690d6f2185b src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Wed Aug 10 09:33:54 2016 +0200
+++ b/src/HOL/Library/FSet.thy	Wed Aug 10 14:50:59 2016 +0200
@@ -528,7 +528,7 @@
 using assms by transfer (metis Set.set_insert finite_insert)
 
 lemma mk_disjoint_finsert: "a |\<in>| A \<Longrightarrow> \<exists>B. A = finsert a B \<and> a |\<notin>| B"
-  by (rule_tac x = "A |-| {|a|}" in exI, blast)
+  by (rule exI [where x = "A |-| {|a|}"]) blast
 
 
 subsubsection \<open>\<open>fimage\<close>\<close>
diff -r f9f3006a5579 -r e690d6f2185b src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Wed Aug 10 09:33:54 2016 +0200
+++ b/src/HOL/Library/IArray.thy	Wed Aug 10 14:50:59 2016 +0200
@@ -71,15 +71,15 @@
 
 lemma [code]:
   "set_iarray as = set (IArray.list_of as)"
-  by (case_tac as) auto
+  by (cases as) auto
 
 lemma [code]:
   "map_iarray f as = IArray (map f (IArray.list_of as))"
-  by (case_tac as) auto
+  by (cases as) auto
 
 lemma [code]:
   "rel_iarray r as bs = list_all2 r (IArray.list_of as) (IArray.list_of bs)"
-  by (case_tac as) (case_tac bs, auto)
+  by (cases as, cases bs) auto
 
 lemma [code]:
   "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
diff -r f9f3006a5579 -r e690d6f2185b src/HOL/Library/Indicator_Function.thy
--- a/src/HOL/Library/Indicator_Function.thy	Wed Aug 10 09:33:54 2016 +0200
+++ b/src/HOL/Library/Indicator_Function.thy	Wed Aug 10 14:50:59 2016 +0200
@@ -97,12 +97,12 @@
   case True
   then obtain i where "x \<in> A i"
     by auto
-  then have
+  then have *:
     "\<And>n. (indicator (A (n + i)) x :: 'a) = 1"
     "(indicator (\<Union>i. A i) x :: 'a) = 1"
     using incseqD[OF \<open>incseq A\<close>, of i "n + i" for n] \<open>x \<in> A i\<close> by (auto simp: indicator_def)
-  then show ?thesis
-    by (rule_tac LIMSEQ_offset[of _ i]) simp
+  show ?thesis
+    by (rule LIMSEQ_offset[of _ i]) (use * in simp)
 next
   case False
   then show ?thesis by (simp add: indicator_def)
@@ -125,12 +125,12 @@
   case True
   then obtain i where "x \<notin> A i"
     by auto
-  then have
+  then have *:
     "\<And>n. (indicator (A (n + i)) x :: 'a) = 0"
     "(indicator (\<Inter>i. A i) x :: 'a) = 0"
     using decseqD[OF \<open>decseq A\<close>, of i "n + i" for n] \<open>x \<notin> A i\<close> by (auto simp: indicator_def)
-  then show ?thesis
-    by (rule_tac LIMSEQ_offset[of _ i]) simp
+  show ?thesis
+    by (rule LIMSEQ_offset[of _ i]) (use * in simp)
 next
   case False
   then show ?thesis by (simp add: indicator_def)
diff -r f9f3006a5579 -r e690d6f2185b src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Wed Aug 10 09:33:54 2016 +0200
+++ b/src/HOL/Library/Permutation.thy	Wed Aug 10 14:50:59 2016 +0200
@@ -95,7 +95,7 @@
   by auto
 
 proposition cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys"
-  by (drule_tac z = z in perm_remove_perm) auto
+  by (drule perm_remove_perm [where z = z]) auto
 
 proposition cons_perm_eq [iff]: "z#xs <~~> z#ys \<longleftrightarrow> xs <~~> ys"
   by (blast intro: cons_perm_imp_perm)
diff -r f9f3006a5579 -r e690d6f2185b src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Wed Aug 10 09:33:54 2016 +0200
+++ b/src/HOL/Library/Polynomial.thy	Wed Aug 10 14:50:59 2016 +0200
@@ -1330,11 +1330,17 @@
 
 lemma synthetic_div_eq_0_iff:
   "synthetic_div p c = 0 \<longleftrightarrow> degree p = 0"
-  by (induct p, simp, case_tac p, simp)
+proof (induct p)
+  case 0
+  then show ?case by simp
+next
+  case (pCons a p)
+  then show ?case by (cases p) simp
+qed
 
 lemma degree_synthetic_div:
   "degree (synthetic_div p c) = degree p - 1"
-  by (induct p, simp, simp add: synthetic_div_eq_0_iff)
+  by (induct p) (simp_all add: synthetic_div_eq_0_iff)
 
 lemma synthetic_div_correct:
   "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)"
@@ -3479,35 +3485,40 @@
 qed (insert assms, auto)
 
 lemma poly_pinfty_gt_lc:
-  fixes p:: "real poly"
-  assumes  "lead_coeff p > 0" 
-  shows "\<exists> n. \<forall> x \<ge> n. poly p x \<ge> lead_coeff p" using assms
+  fixes p :: "real poly"
+  assumes "lead_coeff p > 0" 
+  shows "\<exists> n. \<forall> x \<ge> n. poly p x \<ge> lead_coeff p"
+  using assms
 proof (induct p)
   case 0
-  thus ?case by auto
+  then show ?case by auto
 next
   case (pCons a p)
-  have "\<lbrakk>a\<noteq>0;p=0\<rbrakk> \<Longrightarrow> ?case" by auto
-  moreover have "p\<noteq>0 \<Longrightarrow> ?case"
+  from this(1) consider "a \<noteq> 0" "p = 0" | "p \<noteq> 0" by auto
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis by auto
+  next
+    case 2
+    with pCons obtain n1 where gte_lcoeff: "\<forall>x\<ge>n1. lead_coeff p \<le> poly p x"
+      by auto
+    from pCons(3) \<open>p \<noteq> 0\<close> have gt_0: "lead_coeff p > 0" by auto
+    define n where "n = max n1 (1 + \<bar>a\<bar> / lead_coeff p)"
+    have "lead_coeff (pCons a p) \<le> poly (pCons a p) x" if "n \<le> x" for x
     proof -
-      assume "p\<noteq>0"
-      then obtain n1 where gte_lcoeff:"\<forall>x\<ge>n1. lead_coeff p \<le> poly p x" using that pCons by auto
-      have gt_0:"lead_coeff p >0" using pCons(3) \<open>p\<noteq>0\<close> by auto
-      define n where "n = max n1 (1+ \<bar>a\<bar>/(lead_coeff p))"
-      show ?thesis 
-        proof (rule_tac x=n in exI,rule,rule) 
-          fix x assume "n \<le> x"
-          hence "lead_coeff p \<le> poly p x" 
-            using gte_lcoeff unfolding n_def by auto
-          hence " \<bar>a\<bar>/(lead_coeff p) \<ge> \<bar>a\<bar>/(poly p x)" and "poly p x>0" using gt_0
-            by (intro frac_le,auto)
-          hence "x\<ge>1+ \<bar>a\<bar>/(poly p x)" using \<open>n\<le>x\<close>[unfolded n_def] by auto
-          thus "lead_coeff (pCons a p) \<le> poly (pCons a p) x"
-            using \<open>lead_coeff p \<le> poly p x\<close> \<open>poly p x>0\<close> \<open>p\<noteq>0\<close>
-            by (auto simp add:field_simps)
-        qed
+      from gte_lcoeff that have "lead_coeff p \<le> poly p x"
+        by (auto simp: n_def)
+      with gt_0 have "\<bar>a\<bar> / lead_coeff p \<ge> \<bar>a\<bar> / poly p x" and "poly p x > 0"
+        by (auto intro: frac_le)
+      with \<open>n\<le>x\<close>[unfolded n_def] have "x \<ge> 1 + \<bar>a\<bar> / poly p x"
+        by auto
+      with \<open>lead_coeff p \<le> poly p x\<close> \<open>poly p x > 0\<close> \<open>p \<noteq> 0\<close>
+      show "lead_coeff (pCons a p) \<le> poly (pCons a p) x"
+        by (auto simp: field_simps)
     qed
-  ultimately show ?case by fastforce
+    then show ?thesis by blast
+  qed
 qed
 
 
@@ -3831,9 +3842,7 @@
   "rsquarefree p = (p \<noteq> 0 & (\<forall>a. (order a p = 0) | (order a p = 1)))"
 
 lemma pderiv_iszero: "pderiv p = 0 \<Longrightarrow> \<exists>h. p = [:h :: 'a :: {semidom,semiring_char_0}:]"
-apply (simp add: pderiv_eq_0_iff)
-apply (case_tac p, auto split: if_splits)
-done
+  by (cases p) (auto simp: pderiv_eq_0_iff split: if_splits)
 
 lemma rsquarefree_roots:
   fixes p :: "'a :: field_char_0 poly"
diff -r f9f3006a5579 -r e690d6f2185b src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Wed Aug 10 09:33:54 2016 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Wed Aug 10 14:50:59 2016 +0200
@@ -145,7 +145,6 @@
   shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
   by (simp add: fun_eq_iff foldl_prs_aux [OF a b])
 
-(* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *)
 lemma foldl_rsp[quot_respect]:
   assumes q1: "Quotient3 R1 Abs1 Rep1"
   and     q2: "Quotient3 R2 Abs2 Rep2"
diff -r f9f3006a5579 -r e690d6f2185b src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Wed Aug 10 09:33:54 2016 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Wed Aug 10 14:50:59 2016 +0200
@@ -531,23 +531,18 @@
   by (simp add: rbt_insertwk_is_rbt rbt_insertw_def)
 
 lemma rbt_lookup_rbt_insertw:
-  assumes "is_rbt t"
-  shows "rbt_lookup (rbt_insert_with f k v t) = (rbt_lookup t)(k \<mapsto> (if k:dom (rbt_lookup t) then f (the (rbt_lookup t k)) v else v))"
-using assms
-unfolding rbt_insertw_def
-by (rule_tac ext) (cases "rbt_lookup t k", auto simp:rbt_lookup_rbt_insertwk dom_def)
+  "is_rbt t \<Longrightarrow>
+    rbt_lookup (rbt_insert_with f k v t) =
+      (rbt_lookup t)(k \<mapsto> (if k \<in> dom (rbt_lookup t) then f (the (rbt_lookup t k)) v else v))"
+  by (rule ext, cases "rbt_lookup t k") (auto simp: rbt_lookup_rbt_insertwk dom_def rbt_insertw_def)
 
 lemma rbt_insert_rbt_sorted: "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_insert k v t)"
   by (simp add: rbt_insertwk_rbt_sorted rbt_insert_def)
 theorem rbt_insert_is_rbt [simp]: "is_rbt t \<Longrightarrow> is_rbt (rbt_insert k v t)"
   by (simp add: rbt_insertwk_is_rbt rbt_insert_def)
 
-lemma rbt_lookup_rbt_insert: 
-  assumes "is_rbt t"
-  shows "rbt_lookup (rbt_insert k v t) = (rbt_lookup t)(k\<mapsto>v)"
-unfolding rbt_insert_def
-using assms
-by (rule_tac ext) (simp add: rbt_lookup_rbt_insertwk split:option.split)
+lemma rbt_lookup_rbt_insert: "is_rbt t \<Longrightarrow> rbt_lookup (rbt_insert k v t) = (rbt_lookup t)(k\<mapsto>v)"
+  by (rule ext) (simp add: rbt_insert_def rbt_lookup_rbt_insertwk split: option.split)
 
 end
 
diff -r f9f3006a5579 -r e690d6f2185b src/HOL/Library/RBT_Mapping.thy
--- a/src/HOL/Library/RBT_Mapping.thy	Wed Aug 10 09:33:54 2016 +0200
+++ b/src/HOL/Library/RBT_Mapping.thy	Wed Aug 10 14:50:59 2016 +0200
@@ -43,7 +43,10 @@
 
 lemma map_entry_Mapping [code]:
   "Mapping.map_entry k f (Mapping t) = Mapping (RBT.map_entry k f t)"
-  apply (transfer fixing: t) by (case_tac "RBT.lookup t k") auto
+  apply (transfer fixing: t)
+  apply (case_tac "RBT.lookup t k")
+   apply auto
+  done
 
 lemma keys_Mapping [code]:
   "Mapping.keys (Mapping t) = set (RBT.keys t)"
diff -r f9f3006a5579 -r e690d6f2185b src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Wed Aug 10 09:33:54 2016 +0200
+++ b/src/HOL/Library/RBT_Set.thy	Wed Aug 10 14:50:59 2016 +0200
@@ -273,12 +273,14 @@
   assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
   assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 \<noteq> rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
   shows "P t"
-using assms
-  apply (induction t)
-  apply simp
-  apply (case_tac "t1 = rbt.Empty")
-  apply simp_all
-done
+  using assms
+proof (induct t)
+  case Empty
+  then show ?case by simp
+next
+  case (Branch x1 t1 x3 x4 t2)
+  then show ?case by (cases "t1 = rbt.Empty") simp_all
+qed
 
 lemma rbt_min_opt_in_set: 
   fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
@@ -372,12 +374,14 @@
   assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
   assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 \<noteq> rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
   shows "P t"
-using assms
-  apply (induction t)
-  apply simp
-  apply (case_tac "t2 = rbt.Empty")
-  apply simp_all
-done
+  using assms
+proof (induct t)
+  case Empty
+  then show ?case by simp
+next
+  case (Branch x1 t1 x3 x4 t2)
+  then show ?case by (cases "t2 = rbt.Empty") simp_all
+qed
 
 lemma rbt_max_opt_in_set: 
   fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
@@ -468,27 +472,26 @@
 using assms unfolding is_empty_empty by transfer (auto intro: rbt_min_eq_rbt_min_opt)
 
 lemma fold_keys_min_top_eq:
-  fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt"
+  fixes t :: "('a::{linorder,bounded_lattice_top}, unit) rbt"
   assumes "\<not> (RBT.is_empty t)"
   shows "fold_keys min t top = fold1_keys min t"
 proof -
   have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold min (RBT_Impl.keys t) top = 
-    List.fold min (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) top"
+      List.fold min (hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t)) top"
     by (simp add: hd_Cons_tl[symmetric])
-  { fix x :: "_ :: {linorder, bounded_lattice_top}" and xs
-    have "List.fold min (x#xs) top = List.fold min xs x"
+  have **: "List.fold min (x # xs) top = List.fold min xs x" for x :: 'a and xs
     by (simp add: inf_min[symmetric])
-  } note ** = this
-  show ?thesis using assms
+  show ?thesis
+    using assms
     unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
     apply transfer 
     apply (case_tac t) 
-    apply simp 
+     apply simp 
     apply (subst *)
-    apply simp
+     apply simp
     apply (subst **)
     apply simp
-  done
+    done
 qed
 
 (* maximum *)
@@ -506,27 +509,26 @@
 using assms unfolding is_empty_empty by transfer (auto intro: rbt_max_eq_rbt_max_opt)
 
 lemma fold_keys_max_bot_eq:
-  fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt"
+  fixes t :: "('a::{linorder,bounded_lattice_bot}, unit) rbt"
   assumes "\<not> (RBT.is_empty t)"
   shows "fold_keys max t bot = fold1_keys max t"
 proof -
   have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold max (RBT_Impl.keys t) bot = 
-    List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot"
+      List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot"
     by (simp add: hd_Cons_tl[symmetric])
-  { fix x :: "_ :: {linorder, bounded_lattice_bot}" and xs
-    have "List.fold max (x#xs) bot = List.fold max xs x"
+  have **: "List.fold max (x # xs) bot = List.fold max xs x" for x :: 'a and xs
     by (simp add: sup_max[symmetric])
-  } note ** = this
-  show ?thesis using assms
+  show ?thesis
+    using assms
     unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
     apply transfer 
     apply (case_tac t) 
-    apply simp 
+     apply simp 
     apply (subst *)
-    apply simp
+     apply simp
     apply (subst **)
     apply simp
-  done
+    done
 qed
 
 end
diff -r f9f3006a5579 -r e690d6f2185b src/HOL/Library/Stream.thy
--- a/src/HOL/Library/Stream.thy	Wed Aug 10 09:33:54 2016 +0200
+++ b/src/HOL/Library/Stream.thy	Wed Aug 10 14:50:59 2016 +0200
@@ -393,7 +393,7 @@
   then show "s = sconst x"
   proof (coinduction arbitrary: s)
     case Eq_stream
-    then have "shd s = x" "sset (stl s) \<subseteq> {x}" by (case_tac [!] s) auto
+    then have "shd s = x" "sset (stl s) \<subseteq> {x}" by (cases s; auto)+
     then have "sset (stl s) = {x}" by (cases "stl s") auto
     with \<open>shd s = x\<close> show ?case by auto
   qed
diff -r f9f3006a5579 -r e690d6f2185b src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Wed Aug 10 09:33:54 2016 +0200
+++ b/src/HOL/Library/Sublist.thy	Wed Aug 10 14:50:59 2016 +0200
@@ -156,10 +156,13 @@
   by (simp_all add: strict_prefix_def cong: conj_cong)
 
 lemma take_strict_prefix: "strict_prefix xs ys \<Longrightarrow> strict_prefix (take n xs) ys"
-  apply (induct n arbitrary: xs ys)
-   apply (case_tac ys; simp)
-  apply (metis prefix_order.less_trans strict_prefixI take_is_prefix)
-  done
+proof (induct n arbitrary: xs ys)
+  case 0
+  then show ?case by (cases ys) simp_all
+next
+  case (Suc n)
+  then show ?case by (metis prefix_order.less_trans strict_prefixI take_is_prefix)
+qed
 
 lemma not_prefix_cases:
   assumes pfx: "\<not> prefix ps ls"
@@ -197,7 +200,8 @@
     and r2: "\<And>x xs y ys. \<lbrakk> x = y; \<not> prefix xs ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"
   shows "P ps ls" using np
 proof (induct ls arbitrary: ps)
-  case Nil then show ?case
+  case Nil
+  then show ?case
     by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base)
 next
   case (Cons y ys)
@@ -215,7 +219,13 @@
 "prefixes (x#xs) = [] # map (op # x) (prefixes xs)"
 
 lemma in_set_prefixes[simp]: "xs \<in> set (prefixes ys) \<longleftrightarrow> prefix xs ys"
-by (induction "xs" arbitrary: "ys"; rename_tac "ys", case_tac "ys"; auto)
+proof (induct xs arbitrary: ys)
+  case Nil
+  then show ?case by (cases ys) auto
+next
+  case (Cons a xs)
+  then show ?case by (cases ys) auto
+qed
 
 lemma length_prefixes[simp]: "length (prefixes xs) = length xs+1"
 by (induction xs) auto