# HG changeset patch
# User wenzelm
# Date 1463163850 -7200
# Node ID a949b2a5f51d01bebe1d00d2144f7dfc17d5cd1b
# Parent  54f16a0a30690d187449141f233c1d639d2a23f0
eliminated use of empty "assms";

diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/BNF_Def.thy	Fri May 13 20:24:10 2016 +0200
@@ -248,7 +248,7 @@
   by (simp add: eq_onp_def)
 
 lemma eq_onp_same_args: "eq_onp P x x = P x"
-  using assms by (auto simp add: eq_onp_def)
+  by (auto simp add: eq_onp_def)
 
 lemma eq_onp_eqD: "eq_onp P = Q \<Longrightarrow> P x = Q x x"
   unfolding eq_onp_def by blast
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/BNF_Wellorder_Constructions.thy
--- a/src/HOL/BNF_Wellorder_Constructions.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/BNF_Wellorder_Constructions.thy	Fri May 13 20:24:10 2016 +0200
@@ -570,7 +570,7 @@
 
 lemma not_ordLess_ordIso:
 "r <o r' \<Longrightarrow> \<not> r =o r'"
-using assms ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast
+using ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast
 
 lemma not_ordLeq_iff_ordLess:
 assumes WELL: "Well_order r" and WELL': "Well_order r'"
@@ -584,7 +584,7 @@
 
 lemma ordLess_transitive[trans]:
 "\<lbrakk>r <o r'; r' <o r''\<rbrakk> \<Longrightarrow> r <o r''"
-using assms ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast
+using ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast
 
 corollary ordLess_trans: "trans ordLess"
 unfolding trans_def using ordLess_transitive by blast
@@ -1003,7 +1003,7 @@
 
 lemma Well_order_dir_image:
 "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Well_order (dir_image r f)"
-using assms unfolding well_order_on_def
+unfolding well_order_on_def
 using Linear_order_dir_image[of r f] wf_dir_image[of "r - Id" f]
   dir_image_minus_Id[of f r]
   subset_inj_on[of f "Field r" "Field(r - Id)"]
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/BNF_Wellorder_Embedding.thy
--- a/src/HOL/BNF_Wellorder_Embedding.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/BNF_Wellorder_Embedding.thy	Fri May 13 20:24:10 2016 +0200
@@ -986,7 +986,7 @@
 
 lemma iso_Field:
 "iso r r' f \<Longrightarrow> f ` (Field r) = Field r'"
-using assms by (auto simp add: iso_def bij_betw_def)
+by (auto simp add: iso_def bij_betw_def)
 
 lemma iso_iff:
 assumes "Well_order r"
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Binomial.thy	Fri May 13 20:24:10 2016 +0200
@@ -1324,7 +1324,7 @@
 proof -
   have "((m+r+k) choose (m+k)) * ((m+k) choose k) =
         fact (m+r + k) div (fact (m + k) * fact (m+r - m)) * (fact (m + k) div (fact k * fact m))"
-    by (simp add: assms binomial_altdef_nat)
+    by (simp add: binomial_altdef_nat)
   also have "... = fact (m+r+k) div (fact r * (fact k * fact m))"
     apply (subst div_mult_div_if_dvd)
     apply (auto simp: algebra_simps fact_fact_dvd_fact)
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Fri May 13 20:24:10 2016 +0200
@@ -1105,7 +1105,7 @@
 proof(auto simp add: natLeq_on_Well_order ordIso_reflexive)
   assume "natLeq_on m =o natLeq_on n"
   then obtain f where "bij_betw f {x. x<m} {x. x<n}"
-  using Field_natLeq_on assms unfolding ordIso_def iso_def[abs_def] by auto
+  using Field_natLeq_on unfolding ordIso_def iso_def[abs_def] by auto
   thus "m = n" using atLeastLessThan_injective2[of f m n]
     unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast
 qed
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Fri May 13 20:24:10 2016 +0200
@@ -297,10 +297,10 @@
   using cSup_least [of "f ` A"] by auto
 
 lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> INFIMUM A f \<le> u"
-  by (auto intro: cINF_lower assms order_trans)
+  by (auto intro: cINF_lower order_trans)
 
 lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPREMUM A f"
-  by (auto intro: cSUP_upper assms order_trans)
+  by (auto intro: cSUP_upper order_trans)
 
 lemma cSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (SUP x:A. c) = c"
   by (intro antisym cSUP_least) (auto intro: cSUP_upper)
@@ -309,10 +309,10 @@
   by (intro antisym cINF_greatest) (auto intro: cINF_lower)
 
 lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> INFIMUM A f \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)"
-  by (metis cINF_greatest cINF_lower assms order_trans)
+  by (metis cINF_greatest cINF_lower order_trans)
 
 lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPREMUM A f \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)"
-  by (metis cSUP_least cSUP_upper assms order_trans)
+  by (metis cSUP_least cSUP_upper order_trans)
 
 lemma less_cINF_D: "bdd_below (f`A) \<Longrightarrow> y < (INF i:A. f i) \<Longrightarrow> i \<in> A \<Longrightarrow> y < f i"
   by (metis cINF_lower less_le_trans)
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Deriv.thy	Fri May 13 20:24:10 2016 +0200
@@ -89,7 +89,7 @@
 
 lemma (in bounded_linear) has_derivative:
   "(g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f (g x)) has_derivative (\<lambda>x. f (g' x))) F"
-  using assms unfolding has_derivative_def
+  unfolding has_derivative_def
   apply safe
   apply (erule bounded_linear_compose [OF bounded_linear])
   apply (drule tendsto)
@@ -537,7 +537,7 @@
 lemma differentiable_divide [simp, derivative_intros]:
   fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
   shows "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> (\<lambda>x. f x / g x) differentiable (at x within s)"
-  unfolding divide_inverse using assms by simp
+  unfolding divide_inverse by simp
 
 lemma differentiable_power [simp, derivative_intros]:
   fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
@@ -742,7 +742,7 @@
 
 lemma field_differentiable_diff[derivative_intros]:
   "(f has_field_derivative f') F \<Longrightarrow> (g has_field_derivative g') F \<Longrightarrow> ((\<lambda>z. f z - g z) has_field_derivative f' - g') F"
-  by (simp only: assms diff_conv_add_uminus field_differentiable_add field_differentiable_minus)
+  by (simp only: diff_conv_add_uminus field_differentiable_add field_differentiable_minus)
 
 corollary DERIV_diff:
   "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Equiv_Relations.thy	Fri May 13 20:24:10 2016 +0200
@@ -266,7 +266,7 @@
 
 lemma congruent2D:
   "congruent2 r1 r2 f \<Longrightarrow> (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2"
-  using assms by (auto simp add: congruent2_def)
+  by (auto simp add: congruent2_def)
 
 text\<open>Abbreviation for the common case where the relations are identical\<close>
 abbreviation
@@ -426,7 +426,7 @@
 
 lemma in_quotient_imp_subset:
 "\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> X \<subseteq> A"
-using assms in_quotient_imp_in_rel equiv_type by fastforce
+using in_quotient_imp_in_rel equiv_type by fastforce
 
 
 subsection \<open>Equivalence relations -- predicate version\<close>
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Groups_Big.thy	Fri May 13 20:24:10 2016 +0200
@@ -181,7 +181,7 @@
 
 lemma distrib:
   "F (\<lambda>x. g x * h x) A = F g A * F h A"
-  using assms by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
+  by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
 
 lemma Sigma:
   "finite A \<Longrightarrow> \<forall>x\<in>A. finite (B x) \<Longrightarrow> F (\<lambda>x. F (g x) (B x)) A = F (case_prod g) (SIGMA x:A. B x)"
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri May 13 20:24:10 2016 +0200
@@ -261,7 +261,6 @@
 subsection {* Interaction of these predicates with our heap transitions *}
 
 lemma list_of_set_ref: "refs_of h q rs \<Longrightarrow> p \<notin> set rs \<Longrightarrow> list_of (Ref.set p v h) q as = list_of h q as"
-using assms
 proof (induct as arbitrary: q rs)
   case Nil thus ?case by simp
 next
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Library/Complete_Partial_Order2.thy
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Fri May 13 20:24:10 2016 +0200
@@ -1552,7 +1552,7 @@
 lemma mcont_SUP [cont_intro, simp]:
   "\<lbrakk> mcont lub ord Union op \<subseteq> f; \<And>y. mcont lub ord Sup op \<le> (\<lambda>x. g x y) \<rbrakk>
   \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. \<Squnion>y\<in>f x. g x y)"
-by(blast intro: mcontI cont_SUP[OF assms] monotone_SUP mcont_mono)
+by(blast intro: mcontI cont_SUP monotone_SUP mcont_mono)
 
 end
 
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Library/ContNotDenum.thy
--- a/src/HOL/Library/ContNotDenum.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/ContNotDenum.thy	Fri May 13 20:24:10 2016 +0200
@@ -37,7 +37,6 @@
   txt \<open>First we construct a sequence of nested intervals, ignoring @{term "range f"}.\<close>
 
   have "\<forall>a b c::real. a < b \<longrightarrow> (\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb})"
-    using assms
     by (auto simp add: not_le cong: conj_cong)
        (metis dense le_less_linear less_linear less_trans order_refl)
   then obtain i j where ij:
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Convex.thy	Fri May 13 20:24:10 2016 +0200
@@ -533,7 +533,7 @@
       by (auto simp: add_pos_pos)
   }
   ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0"
-    using assms by fastforce
+    by fastforce
 qed
 
 lemma convex_on_setsum:
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Fri May 13 20:24:10 2016 +0200
@@ -228,7 +228,7 @@
     by auto (metis Diff_insert_absorb countable_Diff insert_absorb)
 
 lemma countable_vimage: "B \<subseteq> range f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
-  by (metis Int_absorb2 assms countable_image image_vimage_eq)
+  by (metis Int_absorb2 countable_image image_vimage_eq)
 
 lemma surj_countable_vimage: "surj f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
   by (metis countable_vimage top_greatest)
@@ -342,7 +342,7 @@
 
 lemma uncountable_minus_countable:
   "uncountable A \<Longrightarrow> countable B \<Longrightarrow> uncountable (A - B)"
-  using countable_Un[of B "A - B"] assms by auto
+  using countable_Un[of B "A - B"] by auto
 
 lemma countable_Diff_eq [simp]: "countable (A - {x}) = countable A"
   by (meson countable_Diff countable_empty countable_insert uncountable_minus_countable)
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Fri May 13 20:24:10 2016 +0200
@@ -281,7 +281,7 @@
   obtains (real) r where "x = ereal r"
     | (PInf) "x = \<infinity>"
     | (MInf) "x = -\<infinity>"
-  using assms by (cases x) auto
+  by (cases x) auto
 
 lemmas ereal2_cases = ereal_cases[case_product ereal_cases]
 lemmas ereal3_cases = ereal2_cases[case_product ereal_cases]
@@ -1009,7 +1009,6 @@
 lemma ereal_mult_right_mono:
   fixes a b c :: ereal
   shows "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
-  using assms
   apply (cases "c = 0")
   apply simp
   apply (cases rule: ereal3_cases[of a b c])
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/FSet.thy	Fri May 13 20:24:10 2016 +0200
@@ -855,7 +855,7 @@
 
 lemma bind_transfer [transfer_rule]:
   "(rel_fset A ===> (A ===> rel_fset B) ===> rel_fset B) fbind fbind"
-  using assms unfolding rel_fun_def
+  unfolding rel_fun_def
   using bind_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
 
 text \<open>Rules requiring bi-unique, bi-total or right-total relations\<close>
@@ -885,7 +885,7 @@
 
 lemma fSup_transfer [transfer_rule]:
   "bi_unique A \<Longrightarrow> (rel_set (rel_fset A) ===> rel_fset A) Sup Sup"
-  using assms unfolding rel_fun_def
+  unfolding rel_fun_def
   apply clarify
   apply transfer'
   using Sup_fset_transfer[unfolded rel_fun_def] by blast
@@ -908,7 +908,7 @@
 
 lemma card_transfer [transfer_rule]:
   "bi_unique A \<Longrightarrow> (rel_fset A ===> op =) fcard fcard"
-  using assms unfolding rel_fun_def
+  unfolding rel_fun_def
   using card_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
 
 end
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Fraction_Field.thy	Fri May 13 20:24:10 2016 +0200
@@ -278,7 +278,7 @@
 
 lemma less_fract [simp]:
   "\<lbrakk> b \<noteq> 0; d \<noteq> 0 \<rbrakk> \<Longrightarrow> Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)"
-  by (simp add: less_fract_def less_le_not_le ac_simps assms)
+  by (simp add: less_fract_def less_le_not_le ac_simps)
 
 instance
 proof
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/FuncSet.thy	Fri May 13 20:24:10 2016 +0200
@@ -402,17 +402,17 @@
 proof -
   {
     fix f assume "f \<in> PiE (insert x S) T" "x \<notin> S"
-    with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
+    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
       by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
   }
   moreover
   {
     fix f assume "f \<in> PiE (insert x S) T" "x \<in> S"
-    with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
+    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
       by (auto intro!: image_eqI[where x="(f x, f)"] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb)
   }
   ultimately show ?thesis
-    using assms by (auto intro: PiE_fun_upd)
+    by (auto intro: PiE_fun_upd)
 qed
 
 lemma PiE_Int: "Pi\<^sub>E I A \<inter> Pi\<^sub>E I B = Pi\<^sub>E I (\<lambda>x. A x \<inter> B x)"
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Library/Indicator_Function.thy
--- a/src/HOL/Library/Indicator_Function.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Indicator_Function.thy	Fri May 13 20:24:10 2016 +0200
@@ -79,7 +79,7 @@
 lemma setsum_indicator_scaleR[simp]:
   "finite A \<Longrightarrow>
     (\<Sum>x \<in> A. indicator (B x) (g x) *\<^sub>R f x) = (\<Sum>x \<in> {x\<in>A. g x \<in> B x}. f x::'a::real_vector)"
-  using assms by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm simp: indicator_def)
+  by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm simp: indicator_def)
 
 lemma LIMSEQ_indicator_incseq:
   assumes "incseq A"
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri May 13 20:24:10 2016 +0200
@@ -967,7 +967,7 @@
 lemma multiset_cases [cases type]:
   obtains (empty) "M = {#}"
     | (add) N x where "M = N + {#x#}"
-  using assms by (induct M) simp_all
+  by (induct M) simp_all
 
 lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
 by (cases "B = {#}") (auto dest: multi_member_split)
@@ -1455,7 +1455,7 @@
   by (induct n, simp_all)
 
 lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<subseteq># M"
-  by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset subseteq_mset_def)
+  by (auto simp add: mset_less_eqI) (metis count_replicate_mset subseteq_mset_def)
 
 lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
   by (induct D) simp_all
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Library/Nonpos_Ints.thy
--- a/src/HOL/Library/Nonpos_Ints.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Nonpos_Ints.thy	Fri May 13 20:24:10 2016 +0200
@@ -54,7 +54,7 @@
 
 lemma nonpos_IntsI: 
   "x \<in> \<int> \<Longrightarrow> x \<le> 0 \<Longrightarrow> (x :: 'a :: linordered_idom) \<in> \<int>\<^sub>\<le>\<^sub>0"
-  using assms unfolding nonpos_Ints_def Ints_def by auto
+  unfolding nonpos_Ints_def Ints_def by auto
 
 lemma nonpos_Ints_subset_Ints: "\<int>\<^sub>\<le>\<^sub>0 \<subseteq> \<int>"
   unfolding nonpos_Ints_def Ints_def by blast
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Lifting.thy	Fri May 13 20:24:10 2016 +0200
@@ -311,7 +311,7 @@
   using 1 2 unfolding Quotient_alt_def reflp_def rel_fun_def by simp
 
 lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
-  using 1 2 assms unfolding Quotient_alt_def reflp_def by metis
+  using 1 2 unfolding Quotient_alt_def reflp_def by metis
 
 lemma Quotient_total_abs_eq_iff: "Abs x = Abs y \<longleftrightarrow> R x y"
   using Quotient_rel [OF 1] 2 unfolding reflp_def by simp
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/List.thy
--- a/src/HOL/List.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/List.thy	Fri May 13 20:24:10 2016 +0200
@@ -2297,7 +2297,7 @@
 by (induct xs) auto
 
 lemma hd_dropWhile: "dropWhile P xs \<noteq> [] \<Longrightarrow> \<not> P (hd (dropWhile P xs))"
-using assms by (induct xs) auto
+by (induct xs) auto
 
 lemma takeWhile_eq_filter:
   assumes "\<And> x. x \<in> set (dropWhile P xs) \<Longrightarrow> \<not> P x"
@@ -4956,8 +4956,7 @@
 
 lemma filter_insort:
   "sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort_key f x xs) = insort_key f x (filter P xs)"
-  using assms by (induct xs)
-    (auto simp add: sorted_Cons, subst insort_is_Cons, auto)
+  by (induct xs) (auto simp add: sorted_Cons, subst insort_is_Cons, auto)
 
 lemma filter_sort:
   "filter P (sort_key f xs) = sort_key f (filter P xs)"
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Fri May 13 20:24:10 2016 +0200
@@ -1798,7 +1798,6 @@
     \<Longrightarrow> contour_integral (linepath a b) f =
         contour_integral (linepath a (midpoint a b)) f + contour_integral (linepath (midpoint a b) b) f"
   apply (rule contour_integral_split [where c = "midpoint a b" and k = "1/2"])
-  using assms
   apply (auto simp: midpoint_def algebra_simps scaleR_conv_of_real)
   done
 
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri May 13 20:24:10 2016 +0200
@@ -179,7 +179,7 @@
 lemma DERIV_zero_UNIV_unique:
   fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
   shows "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
-by (metis DERIV_zero_unique UNIV_I assms convex_UNIV)
+by (metis DERIV_zero_unique UNIV_I convex_UNIV)
 
 subsection \<open>Some limit theorems about real part of real series etc.\<close>
 
@@ -322,7 +322,7 @@
 
 lemma field_differentiable_minus [derivative_intros]:
   "f field_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) field_differentiable F"
-  using assms unfolding field_differentiable_def
+  unfolding field_differentiable_def
   by (metis field_differentiable_minus)
 
 lemma field_differentiable_add [derivative_intros]:
@@ -1047,7 +1047,6 @@
          \<Longrightarrow> DERIV g (f x) :> inverse (f')"
   unfolding has_field_derivative_def
   apply (rule has_derivative_inverse_strong [of s x f g ])
-  using assms
   by auto
 
 lemma has_complex_derivative_inverse_strong_x:
@@ -1061,7 +1060,6 @@
           \<Longrightarrow> DERIV g y :> inverse (f')"
   unfolding has_field_derivative_def
   apply (rule has_derivative_inverse_strong_x [of s g y f])
-  using assms
   by auto
 
 subsection \<open>Taylor on Complex Numbers\<close>
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Fri May 13 20:24:10 2016 +0200
@@ -984,7 +984,7 @@
   using Ln_exp by blast
 
 lemma Re_Ln [simp]: "z \<noteq> 0 \<Longrightarrow> Re(Ln z) = ln(norm z)"
-  by (metis exp_Ln assms ln_exp norm_exp_eq_Re)
+  by (metis exp_Ln ln_exp norm_exp_eq_Re)
 
 corollary ln_cmod_le:
   assumes z: "z \<noteq> 0"
@@ -1608,7 +1608,7 @@
   hence "(-x) powr a = exp (a * ln (-of_real x))" by (simp add: powr_def)
   also from x have "ln (-of_real x) = Ln (of_real x) + of_real (sgn x) * pi * \<i>"
     by (simp add: Ln_minus Ln_of_real)
-  also from x assms have "exp (a * ...) = cis pi powr (of_real (sgn x) * a) * of_real x powr a"
+  also from x have "exp (a * ...) = cis pi powr (of_real (sgn x) * a) * of_real x powr a"
     by (simp add: powr_def exp_add algebra_simps Ln_of_real cis_conv_exp)
   also note cis_pi
   finally show ?thesis by simp
@@ -1621,7 +1621,7 @@
   apply (simp add: powr_def)
   apply (rule DERIV_transform_at [where d = "norm z" and f = "\<lambda>z. exp (s * Ln z)"])
   apply (auto simp: dist_complex_def)
-  apply (intro derivative_eq_intros | simp add: assms)+
+  apply (intro derivative_eq_intros | simp)+
   apply (simp add: field_simps exp_diff)
   done
 
@@ -1631,7 +1631,7 @@
 lemma has_field_derivative_powr_right:
     "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
   apply (simp add: powr_def)
-  apply (intro derivative_eq_intros | simp add: assms)+
+  apply (intro derivative_eq_intros | simp)+
   done
 
 lemma field_differentiable_powr_right:
@@ -1772,7 +1772,7 @@
 qed
 
 lemma lim_1_over_ln: "((\<lambda>n. 1 / ln(real_of_nat n)) \<longlongrightarrow> 0) sequentially"
-  using lim_1_over_Ln [THEN filterlim_sequentially_Suc [THEN iffD2]] assms
+  using lim_1_over_Ln [THEN filterlim_sequentially_Suc [THEN iffD2]]
   apply (subst filterlim_sequentially_Suc [symmetric])
   apply (simp add: lim_sequentially dist_norm)
   apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide)
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri May 13 20:24:10 2016 +0200
@@ -2427,9 +2427,9 @@
     moreover have "{x - a |x. x \<in> (s - {a})} = ((\<lambda>x. -a+x) ` (s - {a}))"
       by auto
     moreover have "insert a (s - {a}) = insert a s"
-      using assms by auto
+      by auto
     ultimately have ?thesis
-      using assms affine_hull_insert_span[of "a" "s-{a}"] by auto
+      using affine_hull_insert_span[of "a" "s-{a}"] by auto
   }
   ultimately show ?thesis by auto
 qed
@@ -2998,7 +2998,7 @@
   have "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
     using aff_dim_UNIV by auto
   then show "aff_dim (S:: 'n::euclidean_space set) \<le> int(DIM('n))"
-    using assms aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
+    using aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
 qed
 
 lemma affine_dim_equal:
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 13 20:24:10 2016 +0200
@@ -4189,7 +4189,7 @@
 
 lemma additive_content_tagged_division:
     "d tagged_division_of (cbox a b) \<Longrightarrow> setsum (\<lambda>(x,l). content l) d = content (cbox a b)"
-  unfolding operative_tagged_division[OF monoidal_monoid operative_content assms,symmetric]
+  unfolding operative_tagged_division[OF monoidal_monoid operative_content,symmetric]
   using setsum_iterate by blast
 
 
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri May 13 20:24:10 2016 +0200
@@ -1318,7 +1318,6 @@
   by (auto intro!: path_component_mem path_component_refl)
 
 lemma path_component_sym: "path_component s x y \<Longrightarrow> path_component s y x"
-  using assms
   unfolding path_component_def
   apply (erule exE)
   apply (rule_tac x="reversepath g" in exI)
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri May 13 20:24:10 2016 +0200
@@ -2791,7 +2791,7 @@
 lemma closed_contains_Inf:
   fixes S :: "real set"
   shows "S \<noteq> {} \<Longrightarrow> bdd_below S \<Longrightarrow> closed S \<Longrightarrow> Inf S \<in> S"
-  by (metis closure_contains_Inf closure_closed assms)
+  by (metis closure_contains_Inf closure_closed)
 
 lemma closed_subset_contains_Inf:
   fixes A C :: "real set"
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Fri May 13 20:24:10 2016 +0200
@@ -341,7 +341,7 @@
 
 lemma cong_gcd_eq_nat:
     "[(a::nat) = b] (mod m) \<Longrightarrow>gcd a m = gcd b m"
-  by (metis assms cong_gcd_eq_int [transferred])
+  by (metis cong_gcd_eq_int [transferred])
 
 lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
   by (auto simp add: cong_gcd_eq_nat)
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy	Fri May 13 20:24:10 2016 +0200
@@ -943,7 +943,7 @@
 
 lemma integrable_cong:
   "M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integrable M f \<longleftrightarrow> integrable N g"
-  using assms by (simp cong: has_bochner_integral_cong add: integrable.simps)
+  by (simp cong: has_bochner_integral_cong add: integrable.simps)
 
 lemma integrable_cong_AE:
   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
@@ -953,7 +953,7 @@
 
 lemma integral_cong:
   "M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integral\<^sup>L M f = integral\<^sup>L N g"
-  using assms by (simp cong: has_bochner_integral_cong cong del: if_cong add: lebesgue_integral_def)
+  by (simp cong: has_bochner_integral_cong cong del: if_cong add: lebesgue_integral_def)
 
 lemma integral_cong_AE:
   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Probability/Distribution_Functions.thy
--- a/src/HOL/Probability/Distribution_Functions.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Probability/Distribution_Functions.thy	Fri May 13 20:24:10 2016 +0200
@@ -64,7 +64,7 @@
   unfolding cdf_def by (rule measure_nonneg)
 
 lemma cdf_bounded: "cdf M x \<le> measure M (space M)"
-  unfolding cdf_def using assms by (intro bounded_measure)
+  unfolding cdf_def by (intro bounded_measure)
 
 lemma cdf_lim_infty:
   "((\<lambda>i. cdf M (real i)) \<longlonglongrightarrow> measure M (space M))"
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy	Fri May 13 20:24:10 2016 +0200
@@ -771,7 +771,7 @@
     done
   with M show "subprob_space (join M)"
     by (intro subprob_spaceI)
-       (auto simp: emeasure_join space_subprob_algebra M assms dest: subprob_space.emeasure_space_le_1)
+       (auto simp: emeasure_join space_subprob_algebra M dest: subprob_space.emeasure_space_le_1)
 next
   assume "\<not>(space N \<noteq> {})"
   thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff)
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Probability/Interval_Integral.thy
--- a/src/HOL/Probability/Interval_Integral.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Probability/Interval_Integral.thy	Fri May 13 20:24:10 2016 +0200
@@ -335,13 +335,13 @@
 lemma interval_integral_zero [simp]:
   fixes a b :: ereal
   shows"LBINT x=a..b. 0 = 0" 
-using assms unfolding interval_lebesgue_integral_def einterval_eq 
+unfolding interval_lebesgue_integral_def einterval_eq 
 by simp
 
 lemma interval_integral_const [intro, simp]:
   fixes a b c :: real
   shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)" 
-using assms unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq 
+unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq 
 by (auto simp add:  less_imp_le field_simps measure_def)
 
 lemma interval_integral_cong_AE:
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri May 13 20:24:10 2016 +0200
@@ -923,7 +923,7 @@
 
 lemma nn_integral_monotone_convergence_simple:
   "incseq f \<Longrightarrow> (\<And>i. simple_function M (f i)) \<Longrightarrow> (SUP i. \<integral>\<^sup>S x. f i x \<partial>M) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"
-  using assms nn_integral_monotone_convergence_SUP[of f M]
+  using nn_integral_monotone_convergence_SUP[of f M]
   by (simp add: nn_integral_eq_simple_integral[symmetric] borel_measurable_simple_function)
 
 lemma SUP_simple_integral_sequences:
@@ -986,7 +986,7 @@
   using nn_integral_linear[of f M "\<lambda>x. 0" c] by simp
 
 lemma nn_integral_multc: "f \<in> borel_measurable M \<Longrightarrow> (\<integral>\<^sup>+ x. f x * c \<partial>M) = integral\<^sup>N M f * c"
-  unfolding mult.commute[of _ c] nn_integral_cmult[OF assms] by simp
+  unfolding mult.commute[of _ c] nn_integral_cmult by simp
 
 lemma nn_integral_divide: "f \<in> borel_measurable M \<Longrightarrow> (\<integral>\<^sup>+ x. f x / c \<partial>M) = (\<integral>\<^sup>+ x. f x \<partial>M) / c"
    unfolding divide_ennreal_def by (rule nn_integral_multc)
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri May 13 20:24:10 2016 +0200
@@ -653,7 +653,7 @@
 qed
 
 lemma set_embed_pmf: "set_pmf embed_pmf = {x. f x \<noteq> 0}"
-by(auto simp add: set_pmf_eq assms pmf_embed_pmf)
+by(auto simp add: set_pmf_eq pmf_embed_pmf)
 
 end
 
@@ -1563,7 +1563,7 @@
                 ennreal_of_nat_eq_real_of_nat nn_integral_pmf_of_set)
 
 lemma measure_pmf_of_set: "measure (measure_pmf pmf_of_set) A = card (S \<inter> A) / card S"
-  using emeasure_pmf_of_set[OF assms, of A]
+  using emeasure_pmf_of_set[of A]
   by (simp add: measure_nonneg measure_pmf.emeasure_eq_measure)
 
 end
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Probability/Set_Integral.thy
--- a/src/HOL/Probability/Set_Integral.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Probability/Set_Integral.thy	Fri May 13 20:24:10 2016 +0200
@@ -183,7 +183,6 @@
 lemma set_integral_reflect:
   fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))"
-  using assms
   by (subst lborel_integral_real_affine[where c="-1" and t=0])
      (auto intro!: integral_cong split: split_indicator)
 
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Fri May 13 20:24:10 2016 +0200
@@ -48,7 +48,7 @@
     val thy = Proof_Context.theory_of lthy;
     val (ctxt, stmt) = get_vc thy vc_name
   in
-    Specification.theorem Thm.theoremK NONE
+    Specification.theorem true Thm.theoremK NONE
       (fn thmss => (Local_Theory.background_theory
          (SPARK_VCs.mark_proved vc_name (flat thmss))))
       (Binding.name vc_name, []) [] ctxt stmt false lthy
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Set_Interval.thy	Fri May 13 20:24:10 2016 +0200
@@ -625,7 +625,7 @@
   by (auto simp: min_def)
 
 lemma Ioc_disjoint: "{a<..b} \<inter> {c<..d} = {} \<longleftrightarrow> b \<le> a \<or> d \<le> c \<or> b \<le> c \<or> d \<le> a"
-  using assms by auto
+  by auto
 
 end
 
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Topological_Spaces.thy	Fri May 13 20:24:10 2016 +0200
@@ -1367,7 +1367,7 @@
 
 lemma (in first_countable_topology) sequentially_imp_eventually_at:
   "(\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f \<longlonglongrightarrow> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially) \<Longrightarrow> eventually P (at a)"
-  using assms sequentially_imp_eventually_within [where s=UNIV] by simp
+  using sequentially_imp_eventually_within [where s=UNIV] by simp
 
 lemma LIMSEQ_SEQ_conv1:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Transcendental.thy	Fri May 13 20:24:10 2016 +0200
@@ -2203,7 +2203,7 @@
 
 lemma powr_mult_base:
   fixes x::real shows "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
-  using assms by (auto simp: powr_add)
+  by (auto simp: powr_add)
 
 lemma powr_powr:
   fixes x::real shows "(x powr a) powr b = x powr (a * b)"
diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Transfer.thy	Fri May 13 20:24:10 2016 +0200
@@ -510,7 +510,7 @@
   "right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp"
   "bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp"
   "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp"
-using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def
+unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def
 by fast+
 
 lemma right_unique_transfer [transfer_rule]: