# HG changeset patch
# User paulson
# Date 1563368570 -3600
# Node ID 89830f937e6824fe0e6c9c97f47b6fdc41868ee1
# Parent  b2bedb022a75804bf11800829fe55aa9e5fb301a# Parent  4df0628e8545819209e9dc41bfe618d862d5918a
merged

diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -610,7 +610,7 @@
 proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
   interpret T: bounded_linear T by fact
   have [measurable]: "T \<in> borel_measurable borel"
-    by (intro borel_measurable_continuous_on1 T.continuous_on continuous_on_id)
+    by (intro borel_measurable_continuous_onI T.continuous_on continuous_on_id)
   assume [measurable]: "f \<in> borel_measurable M"
   then show "(\<lambda>x. T (f x)) \<in> borel_measurable M"
     by auto
@@ -2821,7 +2821,7 @@
       have "eventually (\<lambda>n. x \<le> X n) sequentially"
         unfolding filterlim_at_top_ge[where c=x] by auto
       then show "(\<lambda>n. indicator {..X n} x *\<^sub>R f x) \<longlonglongrightarrow> f x"
-        by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
+        by (intro tendsto_eventually) (auto split: split_indicator elim!: eventually_mono)
     qed
     fix n show "AE x in M. norm (indicator {..X n} x *\<^sub>R f x) \<le> norm (f x)"
       by (auto split: split_indicator)
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -599,7 +599,7 @@
     by (force simp add: sets_restrict_space space_restrict_space)
 qed
 
-lemma borel_measurable_continuous_on1: "continuous_on UNIV f \<Longrightarrow> f \<in> borel_measurable borel"
+lemma borel_measurable_continuous_onI: "continuous_on UNIV f \<Longrightarrow> f \<in> borel_measurable borel"
   by (drule borel_measurable_continuous_on_restrict) simp
 
 lemma borel_measurable_continuous_on_if:
@@ -623,7 +623,7 @@
 lemma borel_measurable_continuous_on:
   assumes f: "continuous_on UNIV f" and g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. f (g x)) \<in> borel_measurable M"
-  using measurable_comp[OF g borel_measurable_continuous_on1[OF f]] by (simp add: comp_def)
+  using measurable_comp[OF g borel_measurable_continuous_onI[OF f]] by (simp add: comp_def)
 
 lemma borel_measurable_continuous_on_indicator:
   fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
@@ -1332,7 +1332,7 @@
 subsection "Borel measurable operators"
 
 lemma borel_measurable_norm[measurable]: "norm \<in> borel_measurable borel"
-  by (intro borel_measurable_continuous_on1 continuous_intros)
+  by (intro borel_measurable_continuous_onI continuous_intros)
 
 lemma borel_measurable_sgn [measurable]: "(sgn::'a::real_normed_vector \<Rightarrow> 'a) \<in> borel_measurable borel"
   by (rule borel_measurable_continuous_countable_exceptions[where X="{0}"])
@@ -1460,7 +1460,7 @@
 
 lemma borel_measurable_exp[measurable]:
   "(exp::'a::{real_normed_field,banach}\<Rightarrow>'a) \<in> borel_measurable borel"
-  by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_exp)
+  by (intro borel_measurable_continuous_onI continuous_at_imp_continuous_on ballI isCont_exp)
 
 lemma measurable_real_floor[measurable]:
   "(floor :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
@@ -1479,10 +1479,10 @@
   by simp
 
 lemma borel_measurable_root [measurable]: "root n \<in> borel_measurable borel"
-  by (intro borel_measurable_continuous_on1 continuous_intros)
+  by (intro borel_measurable_continuous_onI continuous_intros)
 
 lemma borel_measurable_sqrt [measurable]: "sqrt \<in> borel_measurable borel"
-  by (intro borel_measurable_continuous_on1 continuous_intros)
+  by (intro borel_measurable_continuous_onI continuous_intros)
 
 lemma borel_measurable_power [measurable (raw)]:
   fixes f :: "_ \<Rightarrow> 'b::{power,real_normed_algebra}"
@@ -1491,22 +1491,22 @@
   by (intro borel_measurable_continuous_on [OF _ f] continuous_intros)
 
 lemma borel_measurable_Re [measurable]: "Re \<in> borel_measurable borel"
-  by (intro borel_measurable_continuous_on1 continuous_intros)
+  by (intro borel_measurable_continuous_onI continuous_intros)
 
 lemma borel_measurable_Im [measurable]: "Im \<in> borel_measurable borel"
-  by (intro borel_measurable_continuous_on1 continuous_intros)
+  by (intro borel_measurable_continuous_onI continuous_intros)
 
 lemma borel_measurable_of_real [measurable]: "(of_real :: _ \<Rightarrow> (_::real_normed_algebra)) \<in> borel_measurable borel"
-  by (intro borel_measurable_continuous_on1 continuous_intros)
+  by (intro borel_measurable_continuous_onI continuous_intros)
 
 lemma borel_measurable_sin [measurable]: "(sin :: _ \<Rightarrow> (_::{real_normed_field,banach})) \<in> borel_measurable borel"
-  by (intro borel_measurable_continuous_on1 continuous_intros)
+  by (intro borel_measurable_continuous_onI continuous_intros)
 
 lemma borel_measurable_cos [measurable]: "(cos :: _ \<Rightarrow> (_::{real_normed_field,banach})) \<in> borel_measurable borel"
-  by (intro borel_measurable_continuous_on1 continuous_intros)
+  by (intro borel_measurable_continuous_onI continuous_intros)
 
 lemma borel_measurable_arctan [measurable]: "arctan \<in> borel_measurable borel"
-  by (intro borel_measurable_continuous_on1 continuous_intros)
+  by (intro borel_measurable_continuous_onI continuous_intros)
 
 lemma\<^marker>\<open>tag important\<close> borel_measurable_complex_iff:
   "f \<in> borel_measurable M \<longleftrightarrow>
@@ -1692,10 +1692,10 @@
   statements are usually done on type classes. \<close>
 
 lemma measurable_enn2ereal[measurable]: "enn2ereal \<in> borel \<rightarrow>\<^sub>M borel"
-  by (intro borel_measurable_continuous_on1 continuous_on_enn2ereal)
+  by (intro borel_measurable_continuous_onI continuous_on_enn2ereal)
 
 lemma measurable_e2ennreal[measurable]: "e2ennreal \<in> borel \<rightarrow>\<^sub>M borel"
-  by (intro borel_measurable_continuous_on1 continuous_on_e2ennreal)
+  by (intro borel_measurable_continuous_onI continuous_on_e2ennreal)
 
 lemma borel_measurable_enn2real[measurable (raw)]:
   "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. enn2real (f x)) \<in> M \<rightarrow>\<^sub>M borel"
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -2844,7 +2844,7 @@
     by (simp add: Lim_at dist_norm inverse_eq_divide)
   show ?thesis
     apply (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right)
-    apply (rule Lim_transform [OF * Lim_eventually])
+    apply (rule Lim_transform [OF * tendsto_eventually])
     using \<open>open S\<close> x apply (force simp: dist_norm open_contains_ball inverse_eq_divide [symmetric] eventually_at)
     done
 qed
@@ -2948,7 +2948,7 @@
     by (simp add: Lim_within dist_norm inverse_eq_divide)
   show ?thesis
     apply (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right)
-    apply (rule Lim_transform [OF * Lim_eventually])
+    apply (rule Lim_transform [OF * tendsto_eventually])
     using linordered_field_no_ub
     apply (force simp: inverse_eq_divide [symmetric] eventually_at)
     done
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -3402,7 +3402,7 @@
       next
         show "(\<lambda>k. if x \<in> (\<Union>m\<le>k. g ` F m) then norm (f x) else 0)
               \<longlonglongrightarrow> (if x \<in> (\<Union>m. g ` F m) then norm (f x) else 0)" for x
-          by (force intro: Lim_eventually eventually_sequentiallyI)
+          by (force intro: tendsto_eventually eventually_sequentiallyI)
       qed auto
     next
       show "(\<lambda>k. if x \<in> (\<Union>m\<le>k. g ` F m) then f x else 0)
@@ -3411,7 +3411,7 @@
         fix m y
         assume "y \<in> F m"
         show "(\<lambda>k. if \<exists>x\<in>{..k}. g y \<in> g ` F x then f (g y) else 0) \<longlonglongrightarrow> f (g y)"
-          using \<open>y \<in> F m\<close> by (force intro: Lim_eventually eventually_sequentiallyI [of m])
+          using \<open>y \<in> F m\<close> by (force intro: tendsto_eventually eventually_sequentiallyI [of m])
       qed
     qed auto
     then show fai: "f absolutely_integrable_on (\<Union>m. g ` F m)"
@@ -3483,7 +3483,7 @@
           unfolding integral_restrict_UNIV image_UN [symmetric] o_def by simp
       next
         show "(\<lambda>k. if x \<in> ?U k then norm (?D x) else 0) \<longlonglongrightarrow> (if x \<in> (\<Union>n. F n) then norm (?D x) else 0)" for x
-          by (force intro: Lim_eventually eventually_sequentiallyI)
+          by (force intro: tendsto_eventually eventually_sequentiallyI)
       qed auto
     next
       show "(\<lambda>k. if x \<in> ?U k then ?D x else 0) \<longlonglongrightarrow> (if x \<in> (\<Union>n. F n) then ?D x else 0)" for x
@@ -3491,7 +3491,7 @@
         fix n
         assume "x \<in> F n"
         show "(\<lambda>m. if \<exists>j\<in>{..m}. x \<in> F j then ?D x else 0) \<longlonglongrightarrow> ?D x"
-          using \<open>x \<in> F n\<close> by (auto intro!: Lim_eventually eventually_sequentiallyI [of n])
+          using \<open>x \<in> F n\<close> by (auto intro!: tendsto_eventually eventually_sequentiallyI [of n])
       qed
     qed auto
     then show Dai: "?D absolutely_integrable_on (\<Union>n. F n)"
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -1299,11 +1299,11 @@
 lemma continuous_at_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z) Ln"
   by (simp add: field_differentiable_imp_continuous_at field_differentiable_within_Ln)
 
-lemma isCont_Ln' [simp]:
+lemma isCont_Ln' [simp,continuous_intros]:
    "\<lbrakk>isCont f z; f z \<notin> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. Ln (f x)) z"
   by (blast intro: isCont_o2 [OF _ continuous_at_Ln])
 
-lemma continuous_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within S) Ln"
+lemma continuous_within_Ln [continuous_intros]: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within S) Ln"
   using continuous_at_Ln continuous_at_imp_continuous_within by blast
 
 lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> S \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on S Ln"
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -1000,7 +1000,7 @@
           done
         then show ?thesis
           apply (simp add: lim_at_infinity_0)
-          apply (rule Lim_eventually)
+          apply (rule tendsto_eventually)
           apply (simp add: eventually_at)
           apply (rule_tac x=r in exI)
           apply (simp add: \<open>0 < r\<close> dist_norm)
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -2340,7 +2340,7 @@
   have [tendsto_intros]: "((\<lambda>x. \<Sum>i. ?e i x) \<longlongrightarrow> A) ?F"
     by (auto intro!: swap_uniform_limit[where f="\<lambda>n x. \<Sum>i < n. ?e i x" and F = sequentially])
   have [tendsto_intros]: "((\<lambda>x. if x = t then 0 else 1) \<longlongrightarrow> 1) ?F"
-    by (rule Lim_eventually) (simp add: eventually_at_filter)
+    by (rule tendsto_eventually) (simp add: eventually_at_filter)
   have "((\<lambda>y. ((y - t) / abs (y - t)) *\<^sub>R ((\<Sum>n. ?e n y) - A)) \<longlongrightarrow> 0) (at t within T)"
     unfolding *
     by (rule tendsto_norm_zero_cancel) (auto intro!: tendsto_eq_intros)
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -1325,9 +1325,6 @@
 
 subsection \<open>Limits\<close>
 
-lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f \<longlongrightarrow> l) net"
-  by (rule topological_tendstoI) (auto elim: eventually_mono)
-
 text \<open>The expected monotonicity property.\<close>
 
 lemma Lim_Un:
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -1474,7 +1474,7 @@
   have 2: "\<And>k x. indicat_real (\<Union>m\<le>k. S m) x \<le> (indicat_real (\<Union>m\<le>Suc k. S m) x)"
     by (simp add: indicator_def)
   have 3: "\<And>x. (\<lambda>k. indicat_real (\<Union>m\<le>k. S m) x) \<longlonglongrightarrow> (indicat_real (\<Union>n. S n) x)"
-    by (force simp: indicator_def eventually_sequentially intro: Lim_eventually)
+    by (force simp: indicator_def eventually_sequentially intro: tendsto_eventually)
   have 4: "bounded (range (\<lambda>k. integral UNIV (indicat_real (\<Union>m\<le>k. S m))))"
     by (simp add: 0)
   have *: "indicat_real (\<Union>n. S n) integrable_on UNIV \<and>
@@ -1914,7 +1914,7 @@
   have 2: "\<And>n x::'a. indicat_real (S n) x \<le> (indicat_real (S (Suc n)) x)"
     by (simp add: indicator_leI nest rev_subsetD)
   have 3: "\<And>x. (\<lambda>n. indicat_real (S n) x) \<longlonglongrightarrow> (indicat_real (\<Union>(S ` UNIV)) x)"
-    apply (rule Lim_eventually)
+    apply (rule tendsto_eventually)
     apply (simp add: indicator_def)
     by (metis eventually_sequentiallyI lift_Suc_mono_le nest subsetCE)
   have 4: "bounded (range (\<lambda>n. integral UNIV (indicat_real (S n))))"
@@ -3712,7 +3712,7 @@
     show "\<forall>x\<in>UNIV.
          (\<lambda>n. if x \<in> (\<Union>m\<le>n. s m) then f x else 0)
          \<longlonglongrightarrow> (if x \<in> \<Union>(s ` UNIV) then f x else 0)"
-      by (force intro: Lim_eventually eventually_sequentiallyI)
+      by (force intro: tendsto_eventually eventually_sequentiallyI)
   qed auto
   then show "?F \<longlonglongrightarrow> ?I"
     by (simp only: integral_restrict_UNIV)
@@ -3829,7 +3829,7 @@
     then have "eventually (\<lambda>n. ?f n x = ?fR x) sequentially"
       by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator)
     then show "(\<lambda>n. ?f n x) \<longlonglongrightarrow> ?fR x"
-      by (rule Lim_eventually)
+      by (rule tendsto_eventually)
   qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator)
   then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i. ?f i x) \<partial>lborel)"
     by simp
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Analysis/Extended_Real_Limits.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -849,7 +849,7 @@
   then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   then have "min x n = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
   then have "eventually (\<lambda>n. min x n = x) sequentially" using eventually_at_top_linorder by blast
-  then show ?thesis by (simp add: Lim_eventually)
+  then show ?thesis by (simp add: tendsto_eventually)
 next
   case (PInf)
   then have "min x n = n" for n::nat by (auto simp add: min_def)
@@ -870,7 +870,7 @@
   then have "min x n = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
   then have "real_of_ereal(min x n) = r" if "n \<ge> K" for n using real that by auto
   then have "eventually (\<lambda>n. real_of_ereal(min x n) = r) sequentially" using eventually_at_top_linorder by blast
-  then have "(\<lambda>n. real_of_ereal(min x n)) \<longlonglongrightarrow> r" by (simp add: Lim_eventually)
+  then have "(\<lambda>n. real_of_ereal(min x n)) \<longlonglongrightarrow> r" by (simp add: tendsto_eventually)
   then show ?thesis using real by auto
 next
   case (PInf)
@@ -886,7 +886,7 @@
   then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   then have "max x (-real n) = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
   then have "eventually (\<lambda>n. max x (-real n) = x) sequentially" using eventually_at_top_linorder by blast
-  then show ?thesis by (simp add: Lim_eventually)
+  then show ?thesis by (simp add: tendsto_eventually)
 next
   case (MInf)
   then have "max x (-real n) = (-1)* ereal(real n)" for n::nat by (auto simp add: max_def)
@@ -909,7 +909,7 @@
   then have "max x (-real n) = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
   then have "real_of_ereal(max x (-real n)) = r" if "n \<ge> K" for n using real that by auto
   then have "eventually (\<lambda>n. real_of_ereal(max x (-real n)) = r) sequentially" using eventually_at_top_linorder by blast
-  then have "(\<lambda>n. real_of_ereal(max x (-real n))) \<longlonglongrightarrow> r" by (simp add: Lim_eventually)
+  then have "(\<lambda>n. real_of_ereal(max x (-real n))) \<longlonglongrightarrow> r" by (simp add: tendsto_eventually)
   then show ?thesis using real by auto
 next
   case (MInf)
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Analysis/Finite_Product_Measure.thy
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -1224,7 +1224,7 @@
 
 lemma measurable_product_coordinates [measurable (raw)]:
   "(\<lambda>x. x i) \<in> measurable borel borel"
-by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])
+by (rule borel_measurable_continuous_onI[OF continuous_on_product_coordinates])
 
 lemma measurable_product_then_coordinatewise:
   fixes f::"'a \<Rightarrow> 'b \<Rightarrow> ('c::topological_space)"
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -7447,7 +7447,7 @@
       by (simp add: filterlim_at_top)
     with x have "eventually (\<lambda>n. f n x = x powr e) at_top"
       by (auto elim!: eventually_mono simp: f_def)
-    thus "(\<lambda>n. f n x) \<longlonglongrightarrow> x powr e" by (simp add: Lim_eventually)
+    thus "(\<lambda>n. f n x) \<longlonglongrightarrow> x powr e" by (simp add: tendsto_eventually)
   next
     have "norm (integral {a..} (f n)) \<le> -F a" for n :: nat
     proof (cases "n \<ge> a")
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Analysis/Improper_Integral.thy
--- a/src/HOL/Analysis/Improper_Integral.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Improper_Integral.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -1335,7 +1335,7 @@
         by (blast intro: equiintegrable_on_subset [OF equiintegrable_closed_interval_restrictions [OF int_f']])
       have 2: "(\<lambda>n. if x \<in> cbox (u n) (v n) then if x \<in> S then 0 else f x else 0)
                \<longlonglongrightarrow> (if x \<in> cbox c d then if x \<in> S then 0 else f x else 0)" for x
-        by (fastforce simp: dest: get_n intro: Lim_eventually eventually_sequentiallyI)
+        by (fastforce simp: dest: get_n intro: tendsto_eventually eventually_sequentiallyI)
       have [simp]: "cbox c d \<inter> cbox a b = cbox c d"
         using c d by (force simp: mem_box)
       have [simp]: "cbox (u n) (v n) \<inter> cbox a b = cbox (u n) (v n)" for n
@@ -1529,7 +1529,7 @@
           show "?\<phi> k x \<le> ?\<phi> (Suc k) x" if "x \<in> box a b" for k x
             using cb12 box_subset_cbox that by (force simp: intro!: fg)
           show "(\<lambda>k. ?\<phi> k x) \<longlonglongrightarrow> g x - f x \<bullet> j" if x: "x \<in> box a b" for x
-          proof (rule Lim_eventually)
+          proof (rule tendsto_eventually)
             obtain N::nat where N: "\<And>k. k \<ge> N \<Longrightarrow> x \<in> cbox (a + (b - a) /\<^sub>R real k) (b - (b - a) /\<^sub>R real k)"
               using getN [OF x] by blast
             show "\<forall>\<^sub>F k in sequentially. ?\<phi> k x = g x - f x \<bullet> j"
@@ -1609,7 +1609,7 @@
           show "?\<phi> k x \<le> ?\<phi> (Suc k) x" if "x \<in> box a b" for k x
             using cb12 box_subset_cbox that by (force simp: intro!: gf)
           show "(\<lambda>k. ?\<phi> k x) \<longlonglongrightarrow> f x \<bullet> j - g x" if x: "x \<in> box a b" for x
-          proof (rule Lim_eventually)
+          proof (rule tendsto_eventually)
             obtain N::nat where N: "\<And>k. k \<ge> N \<Longrightarrow> x \<in> cbox (a + (b - a) /\<^sub>R real k) (b - (b - a) /\<^sub>R real k)"
               using getN [OF x] by blast
             show "\<forall>\<^sub>F k in sequentially. ?\<phi> k x = f x \<bullet> j - g x"
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -1673,7 +1673,7 @@
     by (force simp add: eventually_sequentially intro: that)
   qed
   with \<theta>to\<Theta> have "(\<lambda>n. (\<Sum>j\<le>n. Im (Ln (z j)))) \<longlonglongrightarrow> \<Theta> + of_int K * (2*pi)"
-    by (simp add: k tendsto_add tendsto_mult Lim_eventually)
+    by (simp add: k tendsto_add tendsto_mult tendsto_eventually)
   moreover have "(\<lambda>n. (\<Sum>k\<le>n. Re (Ln (z k)))) \<longlonglongrightarrow> Re (Ln \<xi>)"
     using assms continuous_imp_tendsto [OF isCont_ln tendsto_norm [OF L]]
     by (simp add: o_def flip: prod_norm ln_prod)
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -518,7 +518,7 @@
       then have "eventually (\<lambda>i. f x * indicator {l i..u i} x = f x) sequentially"
         by eventually_elim auto }
     then show ?thesis
-      unfolding approx(1) by (auto intro!: AE_I2 Lim_eventually split: split_indicator)
+      unfolding approx(1) by (auto intro!: AE_I2 tendsto_eventually split: split_indicator)
   qed
   have 4: "(\<lambda>i. \<integral> x. indicator {l i..u i} x *\<^sub>R f x \<partial>lborel) \<longlonglongrightarrow> C"
     using lbint_lim by (simp add: interval_integral_Icc [unfolded set_lebesgue_integral_def] approx less_imp_le)
@@ -556,7 +556,7 @@
     show "\<And>i. AE x in lborel. norm (indicator {l i..u i} x *\<^sub>R f x) \<le> norm (indicator (einterval a b) x *\<^sub>R f x)"
       by (intro AE_I2) (auto simp: approx split: split_indicator)
     show "AE x in lborel. (\<lambda>i. indicator {l i..u i} x *\<^sub>R f x) \<longlonglongrightarrow> indicator (einterval a b) x *\<^sub>R f x"
-    proof (intro AE_I2 tendsto_intros Lim_eventually)
+    proof (intro AE_I2 tendsto_intros tendsto_eventually)
       fix x
       { fix i assume "l i \<le> x" "x \<le> u i"
         with \<open>incseq u\<close>[THEN incseqD, of i] \<open>decseq l\<close>[THEN decseqD, of i]
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Analysis/Riemann_Mapping.thy
--- a/src/HOL/Analysis/Riemann_Mapping.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Riemann_Mapping.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -576,7 +576,7 @@
                  (contour_integral (?g z) f - (contour_integral (?g x) f + f x * (z - x))) -
                  (contour_integral (linepath x z) f - f x * (z - x)) /\<^sub>R norm (z - x))
             \<midarrow>x\<rightarrow> 0"
-        apply (rule Lim_eventually)
+        apply (rule tendsto_eventually)
         apply (simp add: eventually_at)
         apply (rule_tac x=d in exI)
         using \<open>d > 0\<close> * by simp
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -397,7 +397,7 @@
       then have *: "eventually (\<lambda>i. x \<in> A i) sequentially"
         using \<open>x \<in> A i\<close> \<open>mono A\<close> by (auto simp: eventually_sequentially mono_def)
       show ?thesis
-        apply (intro Lim_eventually)
+        apply (intro tendsto_eventually)
         using *
         apply eventually_elim
         apply (auto split: split_indicator)
@@ -1002,7 +1002,7 @@
       have "eventually (\<lambda>n. x \<le> X n) sequentially"
         unfolding filterlim_at_top_ge[where c=x] by auto
       then show "(\<lambda>n. indicator {a..X n} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {a..} x *\<^sub>R f x"
-        by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
+        by (intro tendsto_eventually) (auto split: split_indicator elim!: eventually_mono)
     qed
     fix n show "AE x in M. norm (indicator {a..X n} x *\<^sub>R f x) \<le> 
                              indicator {a..} x *\<^sub>R norm (f x)"
@@ -1039,7 +1039,7 @@
       have "eventually (\<lambda>n. x \<ge> X n) sequentially"
         unfolding filterlim_at_bot_le[where c=x] by auto
       then show "(\<lambda>n. indicator {X n..b} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {..b} x *\<^sub>R f x"
-        by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
+        by (intro tendsto_eventually) (auto split: split_indicator elim!: eventually_mono)
     qed
     fix n show "AE x in M. norm (indicator {X n..b} x *\<^sub>R f x) \<le> 
                              indicator {..b} x *\<^sub>R norm (f x)"
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Archimedean_Field.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -26,18 +26,10 @@
       apply (force simp: abs_le_iff bdd_above_def)
       done
   next
+    have *: "\<And>x. x \<in> S \<Longrightarrow> Inf S \<le> x"
+      by (meson abs_le_iff bdd bdd_below_def cInf_lower minus_le_iff)
     show "Sup (uminus ` S) \<le> - Inf S"
-      apply (rule cSup_least)
-      using \<open>S \<noteq> {}\<close>
-       apply force
-      apply clarsimp
-      apply (rule cInf_lower)
-       apply assumption
-      using bdd
-      apply (simp add: bdd_below_def)
-      apply (rule_tac x = "- a" in exI)
-      apply force
-      done
+      using \<open>S \<noteq> {}\<close> by (force intro: * cSup_least)
   qed
   with cSup_abs_le [of "uminus ` S"] assms show ?thesis
     by fastforce
@@ -754,6 +746,9 @@
   finally show "x \<in> \<int>" .
 qed (auto simp: frac_def)
 
+lemma frac_1_eq: "frac (x+1) = frac x"
+  by (simp add: frac_def)
+
 
 subsection \<open>Rounding to the nearest integer\<close>
 
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -6117,19 +6117,6 @@
   apply simp
   done
 
-lemma nat_induct2: "P 0 \<Longrightarrow> P 1 \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (n + 2)) \<Longrightarrow> P (n::nat)"
-  unfolding One_nat_def numeral_2_eq_2
-  apply (induct n rule: nat_less_induct)
-  apply (case_tac n)
-  apply simp
-  apply (rename_tac m)
-  apply (case_tac m)
-  apply simp
-  apply (rename_tac k)
-  apply (case_tac k)
-  apply simp_all
-  done
-
 lemma nat_add_1_add_1: "(n::nat) + 1 + 1 = n + 2"
   by simp
 
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Int.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -1154,7 +1154,12 @@
   fixes x:: "'a :: linordered_idom"
   shows "\<lbrakk>x \<in> Ints; abs x < 1\<rbrakk> \<Longrightarrow> x = 0"
     using Ints_nonzero_abs_ge1 [of x] by auto
-    
+
+lemma Ints_eq_abs_less1:
+  fixes x:: "'a :: linordered_idom"
+  shows "\<lbrakk>x \<in> Ints; y \<in> Ints\<rbrakk> \<Longrightarrow> x = y \<longleftrightarrow> abs (x-y) < 1"
+  using eq_iff_diff_eq_0 by (fastforce intro: Ints_nonzero_abs_less1)
+ 
 
 subsection \<open>The functions \<^term>\<open>nat\<close> and \<^term>\<open>int\<close>\<close>
 
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Library/Discrete.thy
--- a/src/HOL/Library/Discrete.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Library/Discrete.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -332,7 +332,8 @@
     have "(Discrete.sqrt n)^2 < m^2" by linarith
   with power2_less_imp_less have lt_m: "Discrete.sqrt n < m" by blast
   from m_def Suc_sqrt_power2_gt[of "n"]
-    have "m^2 \<le> (Suc(Discrete.sqrt n))^2" by simp
+    have "m^2 \<le> (Suc(Discrete.sqrt n))^2"
+      by linarith
   with power2_nat_le_eq_le have "m \<le> Suc (Discrete.sqrt n)" by blast
   with lt_m have "m = Suc (Discrete.sqrt n)" by simp
   with lhs m_def show ?thesis by fastforce
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -148,11 +148,6 @@
     "(\<And>x y. mono (F x y)) \<Longrightarrow> mono (\<lambda>z x. INF y \<in> X x. F x y z :: 'a :: complete_lattice)"
   by (auto intro!: INF_mono[OF bexI] simp: le_fun_def mono_def)
 
-lemma continuous_on_max:
-  fixes f g :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
-  shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. max (f x) (g x))"
-  by (auto simp: continuous_on_def intro!: tendsto_max)
-
 lemma continuous_on_cmult_ereal:
   "\<bar>c::ereal\<bar> \<noteq> \<infinity> \<Longrightarrow> continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. c * f x)"
   using tendsto_cmult_ereal[of c f "f x" "at x within A" for x]
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -2951,10 +2951,6 @@
   thus "((\<lambda>x. ereal (real_of_ereal (f x))) \<longlongrightarrow> 0) F" by (simp add: zero_ereal_def)
 qed
 
-lemma tendsto_explicit:
-  "f \<longlonglongrightarrow> f0 \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> f0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> S))"
-  unfolding tendsto_def eventually_sequentially by auto
-
 lemma Lim_bounded_PInfty2: "f \<longlonglongrightarrow> l \<Longrightarrow> \<forall>n\<ge>N. f n \<le> ereal B \<Longrightarrow> l \<noteq> \<infinity>"
   using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
 
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Library/Landau_Symbols.thy
--- a/src/HOL/Library/Landau_Symbols.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Library/Landau_Symbols.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -1642,7 +1642,7 @@
 subsection \<open>Asymptotic Equivalence\<close>
 
 (* TODO Move *)
-lemma Lim_eventually: "eventually (\<lambda>x. f x = c) F \<Longrightarrow> filterlim f (nhds c) F"
+lemma tendsto_eventually: "eventually (\<lambda>x. f x = c) F \<Longrightarrow> filterlim f (nhds c) F"
   by (simp add: eventually_mono eventually_nhds_x_imp_x filterlim_iff)
 
 named_theorems asymp_equiv_intros
@@ -1775,13 +1775,13 @@
 next
   case True
   with asymp_equiv_eventually_zeros[OF assms] show ?thesis
-    by (simp add: Lim_eventually)
+    by (simp add: tendsto_eventually)
 qed
 
 lemma asymp_equiv_refl_ev:
   assumes "eventually (\<lambda>x. f x = g x) F"
   shows   "f \<sim>[F] g"
-  by (intro asymp_equivI Lim_eventually)
+  by (intro asymp_equivI tendsto_eventually)
      (insert assms, auto elim!: eventually_mono)
 
 lemma asymp_equiv_sandwich:
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Limits.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -779,6 +779,11 @@
   for c :: "'a::topological_semigroup_mult"
   by (rule tendsto_mult [OF _ tendsto_const])
 
+lemma lim_const_over_n [tendsto_intros]:
+  fixes a :: "'a::real_normed_field"
+  shows "(\<lambda>n. a / of_nat n) \<longlonglongrightarrow> 0"
+  using tendsto_mult [OF tendsto_const [of a] lim_1_over_n] by simp
+
 lemmas continuous_of_real [continuous_intros] =
   bounded_linear.continuous [OF bounded_linear_of_real]
 
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Nat.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -1863,6 +1863,22 @@
 
 end
 
+lemma Nats_diff [simp]:
+  fixes a:: "'a::linordered_idom"
+  assumes "a \<in> \<nat>" "b \<in> \<nat>" "b \<le> a" shows "a - b \<in> \<nat>"
+proof -
+  obtain i where i: "a = of_nat i"
+    using Nats_cases assms by blast
+  obtain j where j: "b = of_nat j"
+    using Nats_cases assms by blast
+  have "j \<le> i"
+    using \<open>b \<le> a\<close> i j of_nat_le_iff by blast
+  then have *: "of_nat i - of_nat j = (of_nat (i-j) :: 'a)"
+    by (simp add: of_nat_diff)
+  then show ?thesis
+    by (simp add: * i j)
+qed
+
 
 subsection \<open>Further arithmetic facts concerning the natural numbers\<close>
 
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/NthRoot.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -226,6 +226,10 @@
 lemma real_root_abs: "0 < n \<Longrightarrow> root n \<bar>x\<bar> = \<bar>root n x\<bar>"
   by (simp add: abs_if real_root_minus)
 
+lemma root_abs_power: "n > 0 \<Longrightarrow> abs (root n (y ^n)) = abs y"
+  using root_sgn_power [of n]
+  by (metis abs_ge_zero power_abs real_root_abs real_root_power_cancel)
+
 lemma real_root_power: "0 < n \<Longrightarrow> root n (x ^ k) = root n x ^ k"
   by (induct k) (simp_all add: real_root_mult)
 
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Parity.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -574,6 +574,28 @@
   \<open>A \<noteq> {}\<close> if \<open>odd (card A)\<close>
   using that by auto
 
+lemma nat_induct2 [case_names 0 1 step]:
+  assumes "P 0" "P 1" and step: "\<And>n::nat. P n \<Longrightarrow> P (n + 2)"
+  shows "P n"
+proof (induct n rule: less_induct)
+  case (less n)
+  show ?case
+  proof (cases "n < Suc (Suc 0)")
+    case True
+    then show ?thesis
+      using assms by (auto simp: less_Suc_eq)
+  next
+    case False
+    then obtain k where k: "n = Suc (Suc k)"
+      by (force simp: not_less nat_le_iff_add)
+    then have "k<n"
+      by simp
+    with less assms have "P (k+2)"
+      by blast
+    then show ?thesis
+      by (simp add: k)
+  qed
+qed
 
 subsection \<open>Parity and powers\<close>
 
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Power.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -476,6 +476,10 @@
 lemma power_strict_mono [rule_format]: "a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n"
   by (induct n) (auto simp: mult_strict_mono le_less_trans [of 0 a b])
 
+lemma power_mono_iff [simp]:
+  shows "\<lbrakk>a \<ge> 0; b \<ge> 0; n>0\<rbrakk> \<Longrightarrow> a ^ n \<le> b ^ n \<longleftrightarrow> a \<le> b"
+  using power_mono [of a b] power_strict_mono [of b a] not_le by auto
+
 text\<open>Lemma for \<open>power_strict_decreasing\<close>\<close>
 lemma power_Suc_less: "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n"
   by (induct n) (auto simp: mult_strict_left_mono)
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Probability/Characteristic_Functions.thy
--- a/src/HOL/Probability/Characteristic_Functions.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Probability/Characteristic_Functions.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -91,7 +91,7 @@
 qed
 
 lemma (in real_distribution) char_measurable [measurable]: "char M \<in> borel_measurable borel"
-  by (auto intro!: borel_measurable_continuous_on1 continuous_at_imp_continuous_on isCont_char)
+  by (auto intro!: borel_measurable_continuous_onI continuous_at_imp_continuous_on isCont_char)
 
 subsection \<open>Independence\<close>
 
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Probability/Distributions.thy
--- a/src/HOL/Probability/Distributions.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Probability/Distributions.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -116,7 +116,7 @@
   show "?X \<longlonglongrightarrow> (\<integral>\<^sup>+x. ennreal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel)"
     apply (intro nn_integral_LIMSEQ)
     apply (auto simp: incseq_def le_fun_def eventually_sequentially
-                split: split_indicator intro!: Lim_eventually)
+                split: split_indicator intro!: tendsto_eventually)
     apply (metis nat_ceiling_le_eq)
     done
 
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Probability/Sinc_Integral.thy
--- a/src/HOL/Probability/Sinc_Integral.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Probability/Sinc_Integral.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -138,7 +138,7 @@
   by (auto simp: isCont_sinc)
 
 lemma borel_measurable_sinc[measurable]: "sinc \<in> borel_measurable borel"
-  by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_sinc)
+  by (intro borel_measurable_continuous_onI continuous_at_imp_continuous_on ballI isCont_sinc)
 
 lemma sinc_AE: "AE x in lborel. sin x / x = sinc x"
   by (rule AE_I [where N = "{0}"], auto)
@@ -205,7 +205,7 @@
   using DERIV_Si by (rule DERIV_isCont)
 
 lemma borel_measurable_Si[measurable]: "Si \<in> borel_measurable borel"
-  by (auto intro: isCont_Si continuous_at_imp_continuous_on borel_measurable_continuous_on1)
+  by (auto intro: isCont_Si continuous_at_imp_continuous_on borel_measurable_continuous_onI)
 
 lemma Si_at_top_LBINT:
   "((\<lambda>t. (LBINT x=0..\<infinity>. exp (-(x * t)) * (x * sin t + cos t) / (1 + x^2))) \<longlongrightarrow> 0) at_top"
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Probability/Weak_Convergence.thy
--- a/src/HOL/Probability/Weak_Convergence.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Probability/Weak_Convergence.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -284,7 +284,7 @@
     "(\<lambda> n. integral\<^sup>L (\<mu> n) f) \<longlonglongrightarrow> integral\<^sup>L M f"
   using assms
   by (intro weak_conv_imp_bdd_ae_continuous_conv)
-     (auto intro!: borel_measurable_continuous_on1 continuous_at_imp_continuous_on)
+     (auto intro!: borel_measurable_continuous_onI continuous_at_imp_continuous_on)
 
 theorem weak_conv_imp_continuity_set_conv:
   fixes f :: "real \<Rightarrow> real"
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Real_Asymp/Multiseries_Expansion.thy
--- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -4611,7 +4611,7 @@
 lemma expands_to_real_imp_filterlim:
   assumes "(f expands_to (c :: real)) basis"
   shows   "(f \<longlongrightarrow> c) at_top"
-  using assms by (auto elim!: expands_to.cases simp: eq_commute[of c] Lim_eventually)
+  using assms by (auto elim!: expands_to.cases simp: eq_commute[of c] tendsto_eventually)
 
 lemma expands_to_MSLNil_imp_filterlim:
   assumes "(f expands_to MS MSLNil f') basis"
@@ -4620,7 +4620,7 @@
   from assms have "eventually (\<lambda>x. f' x = 0) at_top" "eventually (\<lambda>x. f' x = f x) at_top"
     by (auto elim!: expands_to.cases is_expansion_aux.cases[of MSLNil])
   hence "eventually (\<lambda>x. f x = 0) at_top" by eventually_elim auto
-  thus ?thesis by (simp add: Lim_eventually)
+  thus ?thesis by (simp add: tendsto_eventually)
 qed
 
 lemma expands_to_neg_exponent_imp_filterlim:
@@ -5193,7 +5193,7 @@
   hence "eventually (\<lambda>n. of_nat (f n) = (of_nat c :: 'a)) F"
     by eventually_elim simp
   thus "filterlim (\<lambda>n. of_nat (f n)) (nhds (of_nat c :: 'a)) F"
-    by (rule Lim_eventually)
+    by (rule tendsto_eventually)
 qed
 
 lemma tendsto_of_int_iff:
@@ -5210,7 +5210,7 @@
   hence "eventually (\<lambda>n. of_int (f n) = (of_int c :: 'a)) F"
     by eventually_elim simp
   thus "filterlim (\<lambda>n. of_int (f n)) (nhds (of_int c :: 'a)) F"
-    by (rule Lim_eventually)
+    by (rule tendsto_eventually)
 qed
 
 lemma filterlim_at_top_int_iff_filterlim_real:
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Set_Interval.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -1995,6 +1995,20 @@
   finally show ?thesis .
 qed
 
+lemma in_pairs: "F g {2*m..Suc(2*n)} = F (\<lambda>i. g(2*i) \<^bold>* g(Suc(2*i))) {m..n}"
+proof (induction n)
+  case 0
+  show ?case
+    by (cases "m=0") auto
+next
+  case (Suc n)
+  then show ?case
+    by (auto simp: assoc split: if_split_asm)
+qed
+
+lemma in_pairs_0: "F g {..Suc(2*n)} = F (\<lambda>i. g(2*i) \<^bold>* g(Suc(2*i))) {..n}"
+  using in_pairs [of _ 0 n] by (simp add: atLeast0AtMost)
+
 end
 
 lemma sum_natinterval_diff:
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Topological_Spaces.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -782,6 +782,9 @@
 lemma tendsto_bot [simp]: "(f \<longlongrightarrow> a) bot"
   by (simp add: tendsto_def)
 
+lemma tendsto_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> ((\<lambda>x. f x) \<longlongrightarrow> l) net"
+  by (rule topological_tendstoI) (auto elim: eventually_mono)
+
 end
 
 lemma (in topological_space) filterlim_within_subset:
@@ -1142,6 +1145,10 @@
 lemma lim_def: "lim X = (THE L. X \<longlonglongrightarrow> L)"
   unfolding Lim_def ..
 
+lemma tendsto_explicit:
+  "f \<longlonglongrightarrow> f0 \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> f0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> S))"
+  unfolding tendsto_def eventually_sequentially by auto
+
 
 subsection \<open>Monotone sequences and subsequences\<close>
 
@@ -1706,7 +1713,7 @@
 lemma LIM_cong: "a = b \<Longrightarrow> (\<And>x. x \<noteq> b \<Longrightarrow> f x = g x) \<Longrightarrow> l = m \<Longrightarrow> (f \<midarrow>a\<rightarrow> l) \<longleftrightarrow> (g \<midarrow>b\<rightarrow> m)"
   by (simp add: LIM_equal)
 
-lemma LIM_cong_limit: "f \<midarrow>x\<rightarrow> L \<Longrightarrow> K = L \<Longrightarrow> f \<midarrow>x\<rightarrow> K"
+lemma tendsto_cong_limit: "(f \<longlongrightarrow> l) F \<Longrightarrow> k = l \<Longrightarrow> (f \<longlongrightarrow> k) F"
   by simp
 
 lemma tendsto_at_iff_tendsto_nhds: "g \<midarrow>l\<rightarrow> g l \<longleftrightarrow> (g \<longlongrightarrow> g l) (nhds l)"
@@ -2249,6 +2256,26 @@
   for x :: "'a::linorder_topology"
   by (simp add: continuous_within filterlim_at_split)
 
+lemma continuous_on_max [continuous_intros]:
+  fixes f g :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
+  shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. max (f x) (g x))"
+  by (auto simp: continuous_on_def intro!: tendsto_max)
+
+lemma continuous_on_min [continuous_intros]:
+  fixes f g :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
+  shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. min (f x) (g x))"
+  by (auto simp: continuous_on_def intro!: tendsto_min)
+
+lemma continuous_max [continuous_intros]:
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::linorder_topology"
+  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. (max (f x) (g x)))"
+  by (simp add: tendsto_max continuous_def)
+
+lemma continuous_min [continuous_intros]:
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::linorder_topology"
+  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. (min (f x) (g x)))"
+  by (simp add: tendsto_min continuous_def)
+
 text \<open>
   The following open/closed Collect lemmas are ported from
   Sébastien Gouëzel's \<open>Ergodic_Theory\<close>.
diff -r b2bedb022a75 -r 89830f937e68 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Transcendental.thy	Wed Jul 17 14:02:50 2019 +0100
@@ -2919,6 +2919,10 @@
 lemma powr_half_sqrt: "0 \<le> x \<Longrightarrow> x powr (1/2) = sqrt x"
   by (simp add: powr_def root_powr_inverse sqrt_def)
 
+lemma square_powr_half [simp]:
+  fixes x::real shows "x\<^sup>2 powr (1/2) = \<bar>x\<bar>"
+  by (simp add: powr_half_sqrt)
+
 lemma ln_powr_bound: "1 \<le> x \<Longrightarrow> 0 < a \<Longrightarrow> ln x \<le> (x powr a) / a"
   for x :: real
   by (metis exp_gt_zero linear ln_eq_zero_iff ln_exp ln_less_self ln_powr mult.commute
@@ -4586,7 +4590,7 @@
   unfolding continuous_within by (rule tendsto_tan)
 
 lemma LIM_cos_div_sin: "(\<lambda>x. cos(x)/sin(x)) \<midarrow>pi/2\<rightarrow> 0"
-  by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
+  by (rule tendsto_cong_limit, (rule tendsto_intros)+, simp_all)
 
 lemma lemma_tan_total: 
   assumes "0 < y" shows "\<exists>x. 0 < x \<and> x < pi/2 \<and> y < tan x"