eliminated use of empty "assms";
authorwenzelm
Fri May 13 20:24:10 2016 +0200 (2016-05-13)
changeset 63092a949b2a5f51d
parent 63091 54f16a0a3069
child 63093 3081f7719df7
eliminated use of empty "assms";
src/HOL/BNF_Def.thy
src/HOL/BNF_Wellorder_Constructions.thy
src/HOL/BNF_Wellorder_Embedding.thy
src/HOL/Binomial.thy
src/HOL/Cardinals/Cardinal_Order_Relation.thy
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/Deriv.thy
src/HOL/Equiv_Relations.thy
src/HOL/Groups_Big.thy
src/HOL/Imperative_HOL/ex/Linked_Lists.thy
src/HOL/Library/Complete_Partial_Order2.thy
src/HOL/Library/ContNotDenum.thy
src/HOL/Library/Convex.thy
src/HOL/Library/Countable_Set.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Indicator_Function.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Nonpos_Ints.thy
src/HOL/Lifting.thy
src/HOL/List.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Distribution_Functions.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Interval_Integral.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/Set_Integral.thy
src/HOL/SPARK/Tools/spark_commands.ML
src/HOL/Set_Interval.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/BNF_Def.thy	Fri May 13 20:22:02 2016 +0200
     1.2 +++ b/src/HOL/BNF_Def.thy	Fri May 13 20:24:10 2016 +0200
     1.3 @@ -248,7 +248,7 @@
     1.4    by (simp add: eq_onp_def)
     1.5  
     1.6  lemma eq_onp_same_args: "eq_onp P x x = P x"
     1.7 -  using assms by (auto simp add: eq_onp_def)
     1.8 +  by (auto simp add: eq_onp_def)
     1.9  
    1.10  lemma eq_onp_eqD: "eq_onp P = Q \<Longrightarrow> P x = Q x x"
    1.11    unfolding eq_onp_def by blast
     2.1 --- a/src/HOL/BNF_Wellorder_Constructions.thy	Fri May 13 20:22:02 2016 +0200
     2.2 +++ b/src/HOL/BNF_Wellorder_Constructions.thy	Fri May 13 20:24:10 2016 +0200
     2.3 @@ -570,7 +570,7 @@
     2.4  
     2.5  lemma not_ordLess_ordIso:
     2.6  "r <o r' \<Longrightarrow> \<not> r =o r'"
     2.7 -using assms ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast
     2.8 +using ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast
     2.9  
    2.10  lemma not_ordLeq_iff_ordLess:
    2.11  assumes WELL: "Well_order r" and WELL': "Well_order r'"
    2.12 @@ -584,7 +584,7 @@
    2.13  
    2.14  lemma ordLess_transitive[trans]:
    2.15  "\<lbrakk>r <o r'; r' <o r''\<rbrakk> \<Longrightarrow> r <o r''"
    2.16 -using assms ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast
    2.17 +using ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast
    2.18  
    2.19  corollary ordLess_trans: "trans ordLess"
    2.20  unfolding trans_def using ordLess_transitive by blast
    2.21 @@ -1003,7 +1003,7 @@
    2.22  
    2.23  lemma Well_order_dir_image:
    2.24  "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Well_order (dir_image r f)"
    2.25 -using assms unfolding well_order_on_def
    2.26 +unfolding well_order_on_def
    2.27  using Linear_order_dir_image[of r f] wf_dir_image[of "r - Id" f]
    2.28    dir_image_minus_Id[of f r]
    2.29    subset_inj_on[of f "Field r" "Field(r - Id)"]
     3.1 --- a/src/HOL/BNF_Wellorder_Embedding.thy	Fri May 13 20:22:02 2016 +0200
     3.2 +++ b/src/HOL/BNF_Wellorder_Embedding.thy	Fri May 13 20:24:10 2016 +0200
     3.3 @@ -986,7 +986,7 @@
     3.4  
     3.5  lemma iso_Field:
     3.6  "iso r r' f \<Longrightarrow> f ` (Field r) = Field r'"
     3.7 -using assms by (auto simp add: iso_def bij_betw_def)
     3.8 +by (auto simp add: iso_def bij_betw_def)
     3.9  
    3.10  lemma iso_iff:
    3.11  assumes "Well_order r"
     4.1 --- a/src/HOL/Binomial.thy	Fri May 13 20:22:02 2016 +0200
     4.2 +++ b/src/HOL/Binomial.thy	Fri May 13 20:24:10 2016 +0200
     4.3 @@ -1324,7 +1324,7 @@
     4.4  proof -
     4.5    have "((m+r+k) choose (m+k)) * ((m+k) choose k) =
     4.6          fact (m+r + k) div (fact (m + k) * fact (m+r - m)) * (fact (m + k) div (fact k * fact m))"
     4.7 -    by (simp add: assms binomial_altdef_nat)
     4.8 +    by (simp add: binomial_altdef_nat)
     4.9    also have "... = fact (m+r+k) div (fact r * (fact k * fact m))"
    4.10      apply (subst div_mult_div_if_dvd)
    4.11      apply (auto simp: algebra_simps fact_fact_dvd_fact)
     5.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Fri May 13 20:22:02 2016 +0200
     5.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Fri May 13 20:24:10 2016 +0200
     5.3 @@ -1105,7 +1105,7 @@
     5.4  proof(auto simp add: natLeq_on_Well_order ordIso_reflexive)
     5.5    assume "natLeq_on m =o natLeq_on n"
     5.6    then obtain f where "bij_betw f {x. x<m} {x. x<n}"
     5.7 -  using Field_natLeq_on assms unfolding ordIso_def iso_def[abs_def] by auto
     5.8 +  using Field_natLeq_on unfolding ordIso_def iso_def[abs_def] by auto
     5.9    thus "m = n" using atLeastLessThan_injective2[of f m n]
    5.10      unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast
    5.11  qed
     6.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Fri May 13 20:22:02 2016 +0200
     6.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Fri May 13 20:24:10 2016 +0200
     6.3 @@ -297,10 +297,10 @@
     6.4    using cSup_least [of "f ` A"] by auto
     6.5  
     6.6  lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> INFIMUM A f \<le> u"
     6.7 -  by (auto intro: cINF_lower assms order_trans)
     6.8 +  by (auto intro: cINF_lower order_trans)
     6.9  
    6.10  lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPREMUM A f"
    6.11 -  by (auto intro: cSUP_upper assms order_trans)
    6.12 +  by (auto intro: cSUP_upper order_trans)
    6.13  
    6.14  lemma cSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (SUP x:A. c) = c"
    6.15    by (intro antisym cSUP_least) (auto intro: cSUP_upper)
    6.16 @@ -309,10 +309,10 @@
    6.17    by (intro antisym cINF_greatest) (auto intro: cINF_lower)
    6.18  
    6.19  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)"
    6.20 -  by (metis cINF_greatest cINF_lower assms order_trans)
    6.21 +  by (metis cINF_greatest cINF_lower order_trans)
    6.22  
    6.23  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)"
    6.24 -  by (metis cSUP_least cSUP_upper assms order_trans)
    6.25 +  by (metis cSUP_least cSUP_upper order_trans)
    6.26  
    6.27  lemma less_cINF_D: "bdd_below (f`A) \<Longrightarrow> y < (INF i:A. f i) \<Longrightarrow> i \<in> A \<Longrightarrow> y < f i"
    6.28    by (metis cINF_lower less_le_trans)
     7.1 --- a/src/HOL/Deriv.thy	Fri May 13 20:22:02 2016 +0200
     7.2 +++ b/src/HOL/Deriv.thy	Fri May 13 20:24:10 2016 +0200
     7.3 @@ -89,7 +89,7 @@
     7.4  
     7.5  lemma (in bounded_linear) has_derivative:
     7.6    "(g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f (g x)) has_derivative (\<lambda>x. f (g' x))) F"
     7.7 -  using assms unfolding has_derivative_def
     7.8 +  unfolding has_derivative_def
     7.9    apply safe
    7.10    apply (erule bounded_linear_compose [OF bounded_linear])
    7.11    apply (drule tendsto)
    7.12 @@ -537,7 +537,7 @@
    7.13  lemma differentiable_divide [simp, derivative_intros]:
    7.14    fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
    7.15    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)"
    7.16 -  unfolding divide_inverse using assms by simp
    7.17 +  unfolding divide_inverse by simp
    7.18  
    7.19  lemma differentiable_power [simp, derivative_intros]:
    7.20    fixes f g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
    7.21 @@ -742,7 +742,7 @@
    7.22  
    7.23  lemma field_differentiable_diff[derivative_intros]:
    7.24    "(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"
    7.25 -  by (simp only: assms diff_conv_add_uminus field_differentiable_add field_differentiable_minus)
    7.26 +  by (simp only: diff_conv_add_uminus field_differentiable_add field_differentiable_minus)
    7.27  
    7.28  corollary DERIV_diff:
    7.29    "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
     8.1 --- a/src/HOL/Equiv_Relations.thy	Fri May 13 20:22:02 2016 +0200
     8.2 +++ b/src/HOL/Equiv_Relations.thy	Fri May 13 20:24:10 2016 +0200
     8.3 @@ -266,7 +266,7 @@
     8.4  
     8.5  lemma congruent2D:
     8.6    "congruent2 r1 r2 f \<Longrightarrow> (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2"
     8.7 -  using assms by (auto simp add: congruent2_def)
     8.8 +  by (auto simp add: congruent2_def)
     8.9  
    8.10  text\<open>Abbreviation for the common case where the relations are identical\<close>
    8.11  abbreviation
    8.12 @@ -426,7 +426,7 @@
    8.13  
    8.14  lemma in_quotient_imp_subset:
    8.15  "\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> X \<subseteq> A"
    8.16 -using assms in_quotient_imp_in_rel equiv_type by fastforce
    8.17 +using in_quotient_imp_in_rel equiv_type by fastforce
    8.18  
    8.19  
    8.20  subsection \<open>Equivalence relations -- predicate version\<close>
     9.1 --- a/src/HOL/Groups_Big.thy	Fri May 13 20:22:02 2016 +0200
     9.2 +++ b/src/HOL/Groups_Big.thy	Fri May 13 20:24:10 2016 +0200
     9.3 @@ -181,7 +181,7 @@
     9.4  
     9.5  lemma distrib:
     9.6    "F (\<lambda>x. g x * h x) A = F g A * F h A"
     9.7 -  using assms by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
     9.8 +  by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
     9.9  
    9.10  lemma Sigma:
    9.11    "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)"
    10.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri May 13 20:22:02 2016 +0200
    10.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri May 13 20:24:10 2016 +0200
    10.3 @@ -261,7 +261,6 @@
    10.4  subsection {* Interaction of these predicates with our heap transitions *}
    10.5  
    10.6  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"
    10.7 -using assms
    10.8  proof (induct as arbitrary: q rs)
    10.9    case Nil thus ?case by simp
   10.10  next
    11.1 --- a/src/HOL/Library/Complete_Partial_Order2.thy	Fri May 13 20:22:02 2016 +0200
    11.2 +++ b/src/HOL/Library/Complete_Partial_Order2.thy	Fri May 13 20:24:10 2016 +0200
    11.3 @@ -1552,7 +1552,7 @@
    11.4  lemma mcont_SUP [cont_intro, simp]:
    11.5    "\<lbrakk> mcont lub ord Union op \<subseteq> f; \<And>y. mcont lub ord Sup op \<le> (\<lambda>x. g x y) \<rbrakk>
    11.6    \<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. \<Squnion>y\<in>f x. g x y)"
    11.7 -by(blast intro: mcontI cont_SUP[OF assms] monotone_SUP mcont_mono)
    11.8 +by(blast intro: mcontI cont_SUP monotone_SUP mcont_mono)
    11.9  
   11.10  end
   11.11  
    12.1 --- a/src/HOL/Library/ContNotDenum.thy	Fri May 13 20:22:02 2016 +0200
    12.2 +++ b/src/HOL/Library/ContNotDenum.thy	Fri May 13 20:24:10 2016 +0200
    12.3 @@ -37,7 +37,6 @@
    12.4    txt \<open>First we construct a sequence of nested intervals, ignoring @{term "range f"}.\<close>
    12.5  
    12.6    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})"
    12.7 -    using assms
    12.8      by (auto simp add: not_le cong: conj_cong)
    12.9         (metis dense le_less_linear less_linear less_trans order_refl)
   12.10    then obtain i j where ij:
    13.1 --- a/src/HOL/Library/Convex.thy	Fri May 13 20:22:02 2016 +0200
    13.2 +++ b/src/HOL/Library/Convex.thy	Fri May 13 20:24:10 2016 +0200
    13.3 @@ -533,7 +533,7 @@
    13.4        by (auto simp: add_pos_pos)
    13.5    }
    13.6    ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0"
    13.7 -    using assms by fastforce
    13.8 +    by fastforce
    13.9  qed
   13.10  
   13.11  lemma convex_on_setsum:
    14.1 --- a/src/HOL/Library/Countable_Set.thy	Fri May 13 20:22:02 2016 +0200
    14.2 +++ b/src/HOL/Library/Countable_Set.thy	Fri May 13 20:24:10 2016 +0200
    14.3 @@ -228,7 +228,7 @@
    14.4      by auto (metis Diff_insert_absorb countable_Diff insert_absorb)
    14.5  
    14.6  lemma countable_vimage: "B \<subseteq> range f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
    14.7 -  by (metis Int_absorb2 assms countable_image image_vimage_eq)
    14.8 +  by (metis Int_absorb2 countable_image image_vimage_eq)
    14.9  
   14.10  lemma surj_countable_vimage: "surj f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
   14.11    by (metis countable_vimage top_greatest)
   14.12 @@ -342,7 +342,7 @@
   14.13  
   14.14  lemma uncountable_minus_countable:
   14.15    "uncountable A \<Longrightarrow> countable B \<Longrightarrow> uncountable (A - B)"
   14.16 -  using countable_Un[of B "A - B"] assms by auto
   14.17 +  using countable_Un[of B "A - B"] by auto
   14.18  
   14.19  lemma countable_Diff_eq [simp]: "countable (A - {x}) = countable A"
   14.20    by (meson countable_Diff countable_empty countable_insert uncountable_minus_countable)
    15.1 --- a/src/HOL/Library/Extended_Real.thy	Fri May 13 20:22:02 2016 +0200
    15.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri May 13 20:24:10 2016 +0200
    15.3 @@ -281,7 +281,7 @@
    15.4    obtains (real) r where "x = ereal r"
    15.5      | (PInf) "x = \<infinity>"
    15.6      | (MInf) "x = -\<infinity>"
    15.7 -  using assms by (cases x) auto
    15.8 +  by (cases x) auto
    15.9  
   15.10  lemmas ereal2_cases = ereal_cases[case_product ereal_cases]
   15.11  lemmas ereal3_cases = ereal2_cases[case_product ereal_cases]
   15.12 @@ -1009,7 +1009,6 @@
   15.13  lemma ereal_mult_right_mono:
   15.14    fixes a b c :: ereal
   15.15    shows "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
   15.16 -  using assms
   15.17    apply (cases "c = 0")
   15.18    apply simp
   15.19    apply (cases rule: ereal3_cases[of a b c])
    16.1 --- a/src/HOL/Library/FSet.thy	Fri May 13 20:22:02 2016 +0200
    16.2 +++ b/src/HOL/Library/FSet.thy	Fri May 13 20:24:10 2016 +0200
    16.3 @@ -855,7 +855,7 @@
    16.4  
    16.5  lemma bind_transfer [transfer_rule]:
    16.6    "(rel_fset A ===> (A ===> rel_fset B) ===> rel_fset B) fbind fbind"
    16.7 -  using assms unfolding rel_fun_def
    16.8 +  unfolding rel_fun_def
    16.9    using bind_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
   16.10  
   16.11  text \<open>Rules requiring bi-unique, bi-total or right-total relations\<close>
   16.12 @@ -885,7 +885,7 @@
   16.13  
   16.14  lemma fSup_transfer [transfer_rule]:
   16.15    "bi_unique A \<Longrightarrow> (rel_set (rel_fset A) ===> rel_fset A) Sup Sup"
   16.16 -  using assms unfolding rel_fun_def
   16.17 +  unfolding rel_fun_def
   16.18    apply clarify
   16.19    apply transfer'
   16.20    using Sup_fset_transfer[unfolded rel_fun_def] by blast
   16.21 @@ -908,7 +908,7 @@
   16.22  
   16.23  lemma card_transfer [transfer_rule]:
   16.24    "bi_unique A \<Longrightarrow> (rel_fset A ===> op =) fcard fcard"
   16.25 -  using assms unfolding rel_fun_def
   16.26 +  unfolding rel_fun_def
   16.27    using card_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast
   16.28  
   16.29  end
    17.1 --- a/src/HOL/Library/Fraction_Field.thy	Fri May 13 20:22:02 2016 +0200
    17.2 +++ b/src/HOL/Library/Fraction_Field.thy	Fri May 13 20:24:10 2016 +0200
    17.3 @@ -278,7 +278,7 @@
    17.4  
    17.5  lemma less_fract [simp]:
    17.6    "\<lbrakk> b \<noteq> 0; d \<noteq> 0 \<rbrakk> \<Longrightarrow> Fract a b < Fract c d \<longleftrightarrow> (a * d) * (b * d) < (c * b) * (b * d)"
    17.7 -  by (simp add: less_fract_def less_le_not_le ac_simps assms)
    17.8 +  by (simp add: less_fract_def less_le_not_le ac_simps)
    17.9  
   17.10  instance
   17.11  proof
    18.1 --- a/src/HOL/Library/FuncSet.thy	Fri May 13 20:22:02 2016 +0200
    18.2 +++ b/src/HOL/Library/FuncSet.thy	Fri May 13 20:24:10 2016 +0200
    18.3 @@ -402,17 +402,17 @@
    18.4  proof -
    18.5    {
    18.6      fix f assume "f \<in> PiE (insert x S) T" "x \<notin> S"
    18.7 -    with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
    18.8 +    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
    18.9        by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
   18.10    }
   18.11    moreover
   18.12    {
   18.13      fix f assume "f \<in> PiE (insert x S) T" "x \<in> S"
   18.14 -    with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
   18.15 +    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
   18.16        by (auto intro!: image_eqI[where x="(f x, f)"] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb)
   18.17    }
   18.18    ultimately show ?thesis
   18.19 -    using assms by (auto intro: PiE_fun_upd)
   18.20 +    by (auto intro: PiE_fun_upd)
   18.21  qed
   18.22  
   18.23  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)"
    19.1 --- a/src/HOL/Library/Indicator_Function.thy	Fri May 13 20:22:02 2016 +0200
    19.2 +++ b/src/HOL/Library/Indicator_Function.thy	Fri May 13 20:24:10 2016 +0200
    19.3 @@ -79,7 +79,7 @@
    19.4  lemma setsum_indicator_scaleR[simp]:
    19.5    "finite A \<Longrightarrow>
    19.6      (\<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)"
    19.7 -  using assms by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm simp: indicator_def)
    19.8 +  by (auto intro!: setsum.mono_neutral_cong_right split: if_split_asm simp: indicator_def)
    19.9  
   19.10  lemma LIMSEQ_indicator_incseq:
   19.11    assumes "incseq A"
    20.1 --- a/src/HOL/Library/Multiset.thy	Fri May 13 20:22:02 2016 +0200
    20.2 +++ b/src/HOL/Library/Multiset.thy	Fri May 13 20:24:10 2016 +0200
    20.3 @@ -967,7 +967,7 @@
    20.4  lemma multiset_cases [cases type]:
    20.5    obtains (empty) "M = {#}"
    20.6      | (add) N x where "M = N + {#x#}"
    20.7 -  using assms by (induct M) simp_all
    20.8 +  by (induct M) simp_all
    20.9  
   20.10  lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
   20.11  by (cases "B = {#}") (auto dest: multi_member_split)
   20.12 @@ -1455,7 +1455,7 @@
   20.13    by (induct n, simp_all)
   20.14  
   20.15  lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<subseteq># M"
   20.16 -  by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset subseteq_mset_def)
   20.17 +  by (auto simp add: mset_less_eqI) (metis count_replicate_mset subseteq_mset_def)
   20.18  
   20.19  lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
   20.20    by (induct D) simp_all
    21.1 --- a/src/HOL/Library/Nonpos_Ints.thy	Fri May 13 20:22:02 2016 +0200
    21.2 +++ b/src/HOL/Library/Nonpos_Ints.thy	Fri May 13 20:24:10 2016 +0200
    21.3 @@ -54,7 +54,7 @@
    21.4  
    21.5  lemma nonpos_IntsI: 
    21.6    "x \<in> \<int> \<Longrightarrow> x \<le> 0 \<Longrightarrow> (x :: 'a :: linordered_idom) \<in> \<int>\<^sub>\<le>\<^sub>0"
    21.7 -  using assms unfolding nonpos_Ints_def Ints_def by auto
    21.8 +  unfolding nonpos_Ints_def Ints_def by auto
    21.9  
   21.10  lemma nonpos_Ints_subset_Ints: "\<int>\<^sub>\<le>\<^sub>0 \<subseteq> \<int>"
   21.11    unfolding nonpos_Ints_def Ints_def by blast
    22.1 --- a/src/HOL/Lifting.thy	Fri May 13 20:22:02 2016 +0200
    22.2 +++ b/src/HOL/Lifting.thy	Fri May 13 20:24:10 2016 +0200
    22.3 @@ -311,7 +311,7 @@
    22.4    using 1 2 unfolding Quotient_alt_def reflp_def rel_fun_def by simp
    22.5  
    22.6  lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
    22.7 -  using 1 2 assms unfolding Quotient_alt_def reflp_def by metis
    22.8 +  using 1 2 unfolding Quotient_alt_def reflp_def by metis
    22.9  
   22.10  lemma Quotient_total_abs_eq_iff: "Abs x = Abs y \<longleftrightarrow> R x y"
   22.11    using Quotient_rel [OF 1] 2 unfolding reflp_def by simp
    23.1 --- a/src/HOL/List.thy	Fri May 13 20:22:02 2016 +0200
    23.2 +++ b/src/HOL/List.thy	Fri May 13 20:24:10 2016 +0200
    23.3 @@ -2297,7 +2297,7 @@
    23.4  by (induct xs) auto
    23.5  
    23.6  lemma hd_dropWhile: "dropWhile P xs \<noteq> [] \<Longrightarrow> \<not> P (hd (dropWhile P xs))"
    23.7 -using assms by (induct xs) auto
    23.8 +by (induct xs) auto
    23.9  
   23.10  lemma takeWhile_eq_filter:
   23.11    assumes "\<And> x. x \<in> set (dropWhile P xs) \<Longrightarrow> \<not> P x"
   23.12 @@ -4956,8 +4956,7 @@
   23.13  
   23.14  lemma filter_insort:
   23.15    "sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort_key f x xs) = insort_key f x (filter P xs)"
   23.16 -  using assms by (induct xs)
   23.17 -    (auto simp add: sorted_Cons, subst insort_is_Cons, auto)
   23.18 +  by (induct xs) (auto simp add: sorted_Cons, subst insort_is_Cons, auto)
   23.19  
   23.20  lemma filter_sort:
   23.21    "filter P (sort_key f xs) = sort_key f (filter P xs)"
    24.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Fri May 13 20:22:02 2016 +0200
    24.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Fri May 13 20:24:10 2016 +0200
    24.3 @@ -1798,7 +1798,6 @@
    24.4      \<Longrightarrow> contour_integral (linepath a b) f =
    24.5          contour_integral (linepath a (midpoint a b)) f + contour_integral (linepath (midpoint a b) b) f"
    24.6    apply (rule contour_integral_split [where c = "midpoint a b" and k = "1/2"])
    24.7 -  using assms
    24.8    apply (auto simp: midpoint_def algebra_simps scaleR_conv_of_real)
    24.9    done
   24.10  
    25.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri May 13 20:22:02 2016 +0200
    25.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri May 13 20:24:10 2016 +0200
    25.3 @@ -179,7 +179,7 @@
    25.4  lemma DERIV_zero_UNIV_unique:
    25.5    fixes f :: "'a::{real_normed_field, real_inner} \<Rightarrow> 'a"
    25.6    shows "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
    25.7 -by (metis DERIV_zero_unique UNIV_I assms convex_UNIV)
    25.8 +by (metis DERIV_zero_unique UNIV_I convex_UNIV)
    25.9  
   25.10  subsection \<open>Some limit theorems about real part of real series etc.\<close>
   25.11  
   25.12 @@ -322,7 +322,7 @@
   25.13  
   25.14  lemma field_differentiable_minus [derivative_intros]:
   25.15    "f field_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) field_differentiable F"
   25.16 -  using assms unfolding field_differentiable_def
   25.17 +  unfolding field_differentiable_def
   25.18    by (metis field_differentiable_minus)
   25.19  
   25.20  lemma field_differentiable_add [derivative_intros]:
   25.21 @@ -1047,7 +1047,6 @@
   25.22           \<Longrightarrow> DERIV g (f x) :> inverse (f')"
   25.23    unfolding has_field_derivative_def
   25.24    apply (rule has_derivative_inverse_strong [of s x f g ])
   25.25 -  using assms
   25.26    by auto
   25.27  
   25.28  lemma has_complex_derivative_inverse_strong_x:
   25.29 @@ -1061,7 +1060,6 @@
   25.30            \<Longrightarrow> DERIV g y :> inverse (f')"
   25.31    unfolding has_field_derivative_def
   25.32    apply (rule has_derivative_inverse_strong_x [of s g y f])
   25.33 -  using assms
   25.34    by auto
   25.35  
   25.36  subsection \<open>Taylor on Complex Numbers\<close>
    26.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Fri May 13 20:22:02 2016 +0200
    26.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Fri May 13 20:24:10 2016 +0200
    26.3 @@ -984,7 +984,7 @@
    26.4    using Ln_exp by blast
    26.5  
    26.6  lemma Re_Ln [simp]: "z \<noteq> 0 \<Longrightarrow> Re(Ln z) = ln(norm z)"
    26.7 -  by (metis exp_Ln assms ln_exp norm_exp_eq_Re)
    26.8 +  by (metis exp_Ln ln_exp norm_exp_eq_Re)
    26.9  
   26.10  corollary ln_cmod_le:
   26.11    assumes z: "z \<noteq> 0"
   26.12 @@ -1608,7 +1608,7 @@
   26.13    hence "(-x) powr a = exp (a * ln (-of_real x))" by (simp add: powr_def)
   26.14    also from x have "ln (-of_real x) = Ln (of_real x) + of_real (sgn x) * pi * \<i>"
   26.15      by (simp add: Ln_minus Ln_of_real)
   26.16 -  also from x assms have "exp (a * ...) = cis pi powr (of_real (sgn x) * a) * of_real x powr a"
   26.17 +  also from x have "exp (a * ...) = cis pi powr (of_real (sgn x) * a) * of_real x powr a"
   26.18      by (simp add: powr_def exp_add algebra_simps Ln_of_real cis_conv_exp)
   26.19    also note cis_pi
   26.20    finally show ?thesis by simp
   26.21 @@ -1621,7 +1621,7 @@
   26.22    apply (simp add: powr_def)
   26.23    apply (rule DERIV_transform_at [where d = "norm z" and f = "\<lambda>z. exp (s * Ln z)"])
   26.24    apply (auto simp: dist_complex_def)
   26.25 -  apply (intro derivative_eq_intros | simp add: assms)+
   26.26 +  apply (intro derivative_eq_intros | simp)+
   26.27    apply (simp add: field_simps exp_diff)
   26.28    done
   26.29  
   26.30 @@ -1631,7 +1631,7 @@
   26.31  lemma has_field_derivative_powr_right:
   26.32      "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
   26.33    apply (simp add: powr_def)
   26.34 -  apply (intro derivative_eq_intros | simp add: assms)+
   26.35 +  apply (intro derivative_eq_intros | simp)+
   26.36    done
   26.37  
   26.38  lemma field_differentiable_powr_right:
   26.39 @@ -1772,7 +1772,7 @@
   26.40  qed
   26.41  
   26.42  lemma lim_1_over_ln: "((\<lambda>n. 1 / ln(real_of_nat n)) \<longlongrightarrow> 0) sequentially"
   26.43 -  using lim_1_over_Ln [THEN filterlim_sequentially_Suc [THEN iffD2]] assms
   26.44 +  using lim_1_over_Ln [THEN filterlim_sequentially_Suc [THEN iffD2]]
   26.45    apply (subst filterlim_sequentially_Suc [symmetric])
   26.46    apply (simp add: lim_sequentially dist_norm)
   26.47    apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide)
    27.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri May 13 20:22:02 2016 +0200
    27.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri May 13 20:24:10 2016 +0200
    27.3 @@ -2427,9 +2427,9 @@
    27.4      moreover have "{x - a |x. x \<in> (s - {a})} = ((\<lambda>x. -a+x) ` (s - {a}))"
    27.5        by auto
    27.6      moreover have "insert a (s - {a}) = insert a s"
    27.7 -      using assms by auto
    27.8 +      by auto
    27.9      ultimately have ?thesis
   27.10 -      using assms affine_hull_insert_span[of "a" "s-{a}"] by auto
   27.11 +      using affine_hull_insert_span[of "a" "s-{a}"] by auto
   27.12    }
   27.13    ultimately show ?thesis by auto
   27.14  qed
   27.15 @@ -2998,7 +2998,7 @@
   27.16    have "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))"
   27.17      using aff_dim_UNIV by auto
   27.18    then show "aff_dim (S:: 'n::euclidean_space set) \<le> int(DIM('n))"
   27.19 -    using assms aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
   27.20 +    using aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
   27.21  qed
   27.22  
   27.23  lemma affine_dim_equal:
    28.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 13 20:22:02 2016 +0200
    28.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 13 20:24:10 2016 +0200
    28.3 @@ -4189,7 +4189,7 @@
    28.4  
    28.5  lemma additive_content_tagged_division:
    28.6      "d tagged_division_of (cbox a b) \<Longrightarrow> setsum (\<lambda>(x,l). content l) d = content (cbox a b)"
    28.7 -  unfolding operative_tagged_division[OF monoidal_monoid operative_content assms,symmetric]
    28.8 +  unfolding operative_tagged_division[OF monoidal_monoid operative_content,symmetric]
    28.9    using setsum_iterate by blast
   28.10  
   28.11  
    29.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri May 13 20:22:02 2016 +0200
    29.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri May 13 20:24:10 2016 +0200
    29.3 @@ -1318,7 +1318,6 @@
    29.4    by (auto intro!: path_component_mem path_component_refl)
    29.5  
    29.6  lemma path_component_sym: "path_component s x y \<Longrightarrow> path_component s y x"
    29.7 -  using assms
    29.8    unfolding path_component_def
    29.9    apply (erule exE)
   29.10    apply (rule_tac x="reversepath g" in exI)
    30.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri May 13 20:22:02 2016 +0200
    30.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri May 13 20:24:10 2016 +0200
    30.3 @@ -2791,7 +2791,7 @@
    30.4  lemma closed_contains_Inf:
    30.5    fixes S :: "real set"
    30.6    shows "S \<noteq> {} \<Longrightarrow> bdd_below S \<Longrightarrow> closed S \<Longrightarrow> Inf S \<in> S"
    30.7 -  by (metis closure_contains_Inf closure_closed assms)
    30.8 +  by (metis closure_contains_Inf closure_closed)
    30.9  
   30.10  lemma closed_subset_contains_Inf:
   30.11    fixes A C :: "real set"
    31.1 --- a/src/HOL/Number_Theory/Cong.thy	Fri May 13 20:22:02 2016 +0200
    31.2 +++ b/src/HOL/Number_Theory/Cong.thy	Fri May 13 20:24:10 2016 +0200
    31.3 @@ -341,7 +341,7 @@
    31.4  
    31.5  lemma cong_gcd_eq_nat:
    31.6      "[(a::nat) = b] (mod m) \<Longrightarrow>gcd a m = gcd b m"
    31.7 -  by (metis assms cong_gcd_eq_int [transferred])
    31.8 +  by (metis cong_gcd_eq_int [transferred])
    31.9  
   31.10  lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
   31.11    by (auto simp add: cong_gcd_eq_nat)
    32.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Fri May 13 20:22:02 2016 +0200
    32.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Fri May 13 20:24:10 2016 +0200
    32.3 @@ -943,7 +943,7 @@
    32.4  
    32.5  lemma integrable_cong:
    32.6    "M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integrable M f \<longleftrightarrow> integrable N g"
    32.7 -  using assms by (simp cong: has_bochner_integral_cong add: integrable.simps)
    32.8 +  by (simp cong: has_bochner_integral_cong add: integrable.simps)
    32.9  
   32.10  lemma integrable_cong_AE:
   32.11    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
   32.12 @@ -953,7 +953,7 @@
   32.13  
   32.14  lemma integral_cong:
   32.15    "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"
   32.16 -  using assms by (simp cong: has_bochner_integral_cong cong del: if_cong add: lebesgue_integral_def)
   32.17 +  by (simp cong: has_bochner_integral_cong cong del: if_cong add: lebesgue_integral_def)
   32.18  
   32.19  lemma integral_cong_AE:
   32.20    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow>
    33.1 --- a/src/HOL/Probability/Distribution_Functions.thy	Fri May 13 20:22:02 2016 +0200
    33.2 +++ b/src/HOL/Probability/Distribution_Functions.thy	Fri May 13 20:24:10 2016 +0200
    33.3 @@ -64,7 +64,7 @@
    33.4    unfolding cdf_def by (rule measure_nonneg)
    33.5  
    33.6  lemma cdf_bounded: "cdf M x \<le> measure M (space M)"
    33.7 -  unfolding cdf_def using assms by (intro bounded_measure)
    33.8 +  unfolding cdf_def by (intro bounded_measure)
    33.9  
   33.10  lemma cdf_lim_infty:
   33.11    "((\<lambda>i. cdf M (real i)) \<longlonglongrightarrow> measure M (space M))"
    34.1 --- a/src/HOL/Probability/Giry_Monad.thy	Fri May 13 20:22:02 2016 +0200
    34.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Fri May 13 20:24:10 2016 +0200
    34.3 @@ -771,7 +771,7 @@
    34.4      done
    34.5    with M show "subprob_space (join M)"
    34.6      by (intro subprob_spaceI)
    34.7 -       (auto simp: emeasure_join space_subprob_algebra M assms dest: subprob_space.emeasure_space_le_1)
    34.8 +       (auto simp: emeasure_join space_subprob_algebra M dest: subprob_space.emeasure_space_le_1)
    34.9  next
   34.10    assume "\<not>(space N \<noteq> {})"
   34.11    thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff)
    35.1 --- a/src/HOL/Probability/Interval_Integral.thy	Fri May 13 20:22:02 2016 +0200
    35.2 +++ b/src/HOL/Probability/Interval_Integral.thy	Fri May 13 20:24:10 2016 +0200
    35.3 @@ -335,13 +335,13 @@
    35.4  lemma interval_integral_zero [simp]:
    35.5    fixes a b :: ereal
    35.6    shows"LBINT x=a..b. 0 = 0" 
    35.7 -using assms unfolding interval_lebesgue_integral_def einterval_eq 
    35.8 +unfolding interval_lebesgue_integral_def einterval_eq 
    35.9  by simp
   35.10  
   35.11  lemma interval_integral_const [intro, simp]:
   35.12    fixes a b c :: real
   35.13    shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)" 
   35.14 -using assms unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq 
   35.15 +unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq 
   35.16  by (auto simp add:  less_imp_le field_simps measure_def)
   35.17  
   35.18  lemma interval_integral_cong_AE:
    36.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri May 13 20:22:02 2016 +0200
    36.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri May 13 20:24:10 2016 +0200
    36.3 @@ -923,7 +923,7 @@
    36.4  
    36.5  lemma nn_integral_monotone_convergence_simple:
    36.6    "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)"
    36.7 -  using assms nn_integral_monotone_convergence_SUP[of f M]
    36.8 +  using nn_integral_monotone_convergence_SUP[of f M]
    36.9    by (simp add: nn_integral_eq_simple_integral[symmetric] borel_measurable_simple_function)
   36.10  
   36.11  lemma SUP_simple_integral_sequences:
   36.12 @@ -986,7 +986,7 @@
   36.13    using nn_integral_linear[of f M "\<lambda>x. 0" c] by simp
   36.14  
   36.15  lemma nn_integral_multc: "f \<in> borel_measurable M \<Longrightarrow> (\<integral>\<^sup>+ x. f x * c \<partial>M) = integral\<^sup>N M f * c"
   36.16 -  unfolding mult.commute[of _ c] nn_integral_cmult[OF assms] by simp
   36.17 +  unfolding mult.commute[of _ c] nn_integral_cmult by simp
   36.18  
   36.19  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"
   36.20     unfolding divide_ennreal_def by (rule nn_integral_multc)
    37.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri May 13 20:22:02 2016 +0200
    37.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri May 13 20:24:10 2016 +0200
    37.3 @@ -653,7 +653,7 @@
    37.4  qed
    37.5  
    37.6  lemma set_embed_pmf: "set_pmf embed_pmf = {x. f x \<noteq> 0}"
    37.7 -by(auto simp add: set_pmf_eq assms pmf_embed_pmf)
    37.8 +by(auto simp add: set_pmf_eq pmf_embed_pmf)
    37.9  
   37.10  end
   37.11  
   37.12 @@ -1563,7 +1563,7 @@
   37.13                  ennreal_of_nat_eq_real_of_nat nn_integral_pmf_of_set)
   37.14  
   37.15  lemma measure_pmf_of_set: "measure (measure_pmf pmf_of_set) A = card (S \<inter> A) / card S"
   37.16 -  using emeasure_pmf_of_set[OF assms, of A]
   37.17 +  using emeasure_pmf_of_set[of A]
   37.18    by (simp add: measure_nonneg measure_pmf.emeasure_eq_measure)
   37.19  
   37.20  end
    38.1 --- a/src/HOL/Probability/Set_Integral.thy	Fri May 13 20:22:02 2016 +0200
    38.2 +++ b/src/HOL/Probability/Set_Integral.thy	Fri May 13 20:24:10 2016 +0200
    38.3 @@ -183,7 +183,6 @@
    38.4  lemma set_integral_reflect:
    38.5    fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
    38.6    shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))"
    38.7 -  using assms
    38.8    by (subst lborel_integral_real_affine[where c="-1" and t=0])
    38.9       (auto intro!: integral_cong split: split_indicator)
   38.10  
    39.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri May 13 20:22:02 2016 +0200
    39.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Fri May 13 20:24:10 2016 +0200
    39.3 @@ -48,7 +48,7 @@
    39.4      val thy = Proof_Context.theory_of lthy;
    39.5      val (ctxt, stmt) = get_vc thy vc_name
    39.6    in
    39.7 -    Specification.theorem Thm.theoremK NONE
    39.8 +    Specification.theorem true Thm.theoremK NONE
    39.9        (fn thmss => (Local_Theory.background_theory
   39.10           (SPARK_VCs.mark_proved vc_name (flat thmss))))
   39.11        (Binding.name vc_name, []) [] ctxt stmt false lthy
    40.1 --- a/src/HOL/Set_Interval.thy	Fri May 13 20:22:02 2016 +0200
    40.2 +++ b/src/HOL/Set_Interval.thy	Fri May 13 20:24:10 2016 +0200
    40.3 @@ -625,7 +625,7 @@
    40.4    by (auto simp: min_def)
    40.5  
    40.6  lemma Ioc_disjoint: "{a<..b} \<inter> {c<..d} = {} \<longleftrightarrow> b \<le> a \<or> d \<le> c \<or> b \<le> c \<or> d \<le> a"
    40.7 -  using assms by auto
    40.8 +  by auto
    40.9  
   40.10  end
   40.11  
    41.1 --- a/src/HOL/Topological_Spaces.thy	Fri May 13 20:22:02 2016 +0200
    41.2 +++ b/src/HOL/Topological_Spaces.thy	Fri May 13 20:24:10 2016 +0200
    41.3 @@ -1367,7 +1367,7 @@
    41.4  
    41.5  lemma (in first_countable_topology) sequentially_imp_eventually_at:
    41.6    "(\<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)"
    41.7 -  using assms sequentially_imp_eventually_within [where s=UNIV] by simp
    41.8 +  using sequentially_imp_eventually_within [where s=UNIV] by simp
    41.9  
   41.10  lemma LIMSEQ_SEQ_conv1:
   41.11    fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
    42.1 --- a/src/HOL/Transcendental.thy	Fri May 13 20:22:02 2016 +0200
    42.2 +++ b/src/HOL/Transcendental.thy	Fri May 13 20:24:10 2016 +0200
    42.3 @@ -2203,7 +2203,7 @@
    42.4  
    42.5  lemma powr_mult_base:
    42.6    fixes x::real shows "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
    42.7 -  using assms by (auto simp: powr_add)
    42.8 +  by (auto simp: powr_add)
    42.9  
   42.10  lemma powr_powr:
   42.11    fixes x::real shows "(x powr a) powr b = x powr (a * b)"
    43.1 --- a/src/HOL/Transfer.thy	Fri May 13 20:22:02 2016 +0200
    43.2 +++ b/src/HOL/Transfer.thy	Fri May 13 20:24:10 2016 +0200
    43.3 @@ -510,7 +510,7 @@
    43.4    "right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp"
    43.5    "bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp"
    43.6    "bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp"
    43.7 -using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def
    43.8 +unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def
    43.9  by fast+
   43.10  
   43.11  lemma right_unique_transfer [transfer_rule]: