# HG changeset patch
# User wenzelm
# Date 1442864774 -7200
# Node ID 05d28dc76e5c7d6d9b025a620f1c1a76c23aba7e
# Parent  bf194f7c4c8eb2d2745681a4b61c3cbe164d0b7b
isabelle update_cartouches;

diff -r bf194f7c4c8e -r 05d28dc76e5c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Sep 21 21:43:09 2015 +0200
+++ b/src/HOL/HOL.thy	Mon Sep 21 21:46:14 2015 +0200
@@ -1691,8 +1691,8 @@
 \<close>
 
 
-text{* Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
-not to simplify the argument and to solve it by an assumption. *}
+text\<open>Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
+not to simplify the argument and to solve it by an assumption.\<close>
 
 definition ASSUMPTION :: "bool \<Rightarrow> bool" where
 "ASSUMPTION A \<equiv> A"
@@ -1706,7 +1706,7 @@
 lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A"
 by(simp add: ASSUMPTION_def)
 
-setup {*
+setup \<open>
 let
   val asm_sol = mk_solver "ASSUMPTION" (fn ctxt =>
     resolve_tac ctxt [@{thm ASSUMPTION_I}] THEN'
@@ -1714,7 +1714,7 @@
 in
   map_theory_simpset (fn ctxt => Simplifier.addSolver (ctxt,asm_sol))
 end
-*}
+\<close>
 
 
 subsection \<open>Code generator setup\<close>
diff -r bf194f7c4c8e -r 05d28dc76e5c src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Sep 21 21:43:09 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Sep 21 21:46:14 2015 +0200
@@ -81,7 +81,7 @@
     using assms
     by (auto simp: piecewise_differentiable_on_def)
   have finabc: "finite ({a,b,c} \<union> (s \<union> t))"
-    by (metis `finite s` `finite t` finite_Un finite_insert finite.emptyI)
+    by (metis \<open>finite s\<close> \<open>finite t\<close> finite_Un finite_insert finite.emptyI)
   have "continuous_on {a..c} f" "continuous_on {c..b} g"
     using assms piecewise_differentiable_on_def by auto
   then have "continuous_on {a..b} (\<lambda>x. if x \<le> c then f x else g x)"
@@ -462,7 +462,7 @@
     by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
   have "continuous_on {0..1} g1"
     using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast
-  with `finite s` show ?thesis
+  with \<open>finite s\<close> show ?thesis
     apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
     apply (rule_tac x="insert 1 ((op*2)`s)" in exI)
     apply (simp add: g1D con_g1)
@@ -509,7 +509,7 @@
     by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
   have "continuous_on {0..1} g2"
     using continuous_on_joinpaths_D2 assms piecewise_C1_differentiable_on_def by blast
-  with `finite s` show ?thesis
+  with \<open>finite s\<close> show ?thesis
     apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
     apply (rule_tac x="insert 0 ((\<lambda>x. 2 * x - 1) ` s)" in exI)
     apply (simp add: g2D con_g2)
@@ -2253,11 +2253,11 @@
         def shrink \<equiv> "\<lambda>x. x - e *\<^sub>R (x - d)"
         let ?pathint = "\<lambda>x y. path_integral(linepath x y) f"
         have e: "0 < e" "e \<le> 1" "e \<le> d1 / (4 * C)" "e \<le> cmod y / 24 / C / B"
-          using d1_pos `C>0` `B>0` ynz by (simp_all add: e_def)
+          using d1_pos \<open>C>0\<close> \<open>B>0\<close> ynz by (simp_all add: e_def)
         then have eCB: "24 * e * C * B \<le> cmod y"
-          using `C>0` `B>0`  by (simp add: field_simps)
+          using \<open>C>0\<close> \<open>B>0\<close>  by (simp add: field_simps)
         have e_le_d1: "e * (4 * C) \<le> d1"
-          using e `C>0` by (simp add: field_simps)
+          using e \<open>C>0\<close> by (simp add: field_simps)
         have "shrink a \<in> interior(convex hull {a,b,c})"
              "shrink b \<in> interior(convex hull {a,b,c})"
              "shrink c \<in> interior(convex hull {a,b,c})"
@@ -2276,10 +2276,10 @@
         have sh_eq: "\<And>a b d::complex. (b - e *\<^sub>R (b - d)) - (a - e *\<^sub>R (a - d)) - (b - a) = e *\<^sub>R (a - b)"
           by (simp add: algebra_simps)
         have "cmod y / (24 * C) \<le> cmod y / cmod (b - a) / 12"
-          using False `C>0` diff_2C [of b a] ynz
+          using False \<open>C>0\<close> diff_2C [of b a] ynz
           by (auto simp: divide_simps hull_inc)
         have less_C: "\<lbrakk>u \<in> convex hull {a, b, c}; 0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> x * cmod u < C" for x u
-          apply (cases "x=0", simp add: `0<C`)
+          apply (cases "x=0", simp add: \<open>0<C\<close>)
           using Cno [of u] mult_left_le_one_le [of "cmod u" x] le_less_trans norm_ge_zero by blast
         { fix u v
           assume uv: "u \<in> convex hull {a, b, c}" "v \<in> convex hull {a, b, c}" "u\<noteq>v"
@@ -2292,7 +2292,7 @@
             using shr_uv by (blast intro: Bnf linepath_in_convex_hull interior_subset [THEN subsetD])
           have By_uv: "B * (12 * (e * cmod (u - v))) \<le> cmod y"
             apply (rule order_trans [OF _ eCB])
-            using e `B>0` diff_2C [of u v] uv
+            using e \<open>B>0\<close> diff_2C [of u v] uv
             by (auto simp: field_simps)
           { fix x::real   assume x: "0\<le>x" "x\<le>1"
             have cmod_less_4C: "cmod ((1 - x) *\<^sub>R u - (1 - x) *\<^sub>R d) + cmod (x *\<^sub>R v - x *\<^sub>R d) < (C+C) + (C+C)"
@@ -2303,7 +2303,7 @@
             have ll: "linepath (shrink u) (shrink v) x - linepath u v x = -e * ((1 - x) *\<^sub>R (u - d) + x *\<^sub>R (v - d))"
               by (simp add: linepath_def shrink_def algebra_simps scaleR_conv_of_real)
             have cmod_less_dt: "cmod (linepath (shrink u) (shrink v) x - linepath u v x) < d1"
-              using `e>0`
+              using \<open>e>0\<close>
               apply (simp add: ll norm_mult scaleR_diff_right)
               apply (rule less_le_trans [OF _ e_le_d1])
               using cmod_less_4C
@@ -2313,7 +2313,7 @@
               using x uv shr_uv cmod_less_dt
               by (auto simp: hull_inc intro: d1 interior_subset [THEN subsetD] linepath_in_convex_hull)
             also have "... \<le> cmod y / cmod (v - u) / 12"
-              using False uv `C>0` diff_2C [of v u] ynz
+              using False uv \<open>C>0\<close> diff_2C [of v u] ynz
               by (auto simp: divide_simps hull_inc)
             finally have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) \<le> cmod y / cmod (v - u) / 12"
               by simp
@@ -2324,7 +2324,7 @@
                   \<le> cmod y / 6"
               apply (rule order_trans [of _ "B*((norm y / 24 / C / B)*2*C) + (2*C)*(norm y /24 / C)"])
               apply (rule add_mono [OF mult_mono])
-              using By_uv e `0 < B` `0 < C` x ynz
+              using By_uv e \<open>0 < B\<close> \<open>0 < C\<close> x ynz
               apply (simp_all add: cmod_fuv cmod_shr cmod_12_le hull_inc)
               apply (simp add: field_simps)
               done
@@ -2339,7 +2339,7 @@
                     [of "B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)"
                         "\<lambda>x. f(linepath (shrink u) (shrink v) x) * (shrink v - shrink u) - f(linepath u v x)*(v - u)"
                         _ 0 1 ])
-            using ynz `0 < B` `0 < C`
+            using ynz \<open>0 < B\<close> \<open>0 < C\<close>
             apply (simp_all del: le_divide_eq_numeral1)
             apply (simp add: has_integral_sub has_path_integral_linepath [symmetric] has_path_integral_integral
                              fpi_uv f_uv path_integrable_continuous_linepath, clarify)
@@ -2376,7 +2376,7 @@
           by (simp add: contf compact_convex_hull compact_uniformly_continuous)
         ultimately have "False"
           unfolding uniformly_continuous_on_def
-          by (force simp: ynz `0 < C` dist_norm)
+          by (force simp: ynz \<open>0 < C\<close> dist_norm)
         then show ?thesis ..
       qed
   }
@@ -2411,7 +2411,7 @@
       case False
       show "(f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
         apply (rule less.hyps [of "s'"])
-        using False d `finite s` interior_subset
+        using False d \<open>finite s\<close> interior_subset
         apply (auto intro!: less.prems)
         done
     next
@@ -2420,7 +2420,7 @@
         by (meson True hull_subset insert_subset convex_hull_subset)
       have abd: "(f has_path_integral 0) (linepath a b +++ linepath b d +++ linepath d a)"
         apply (rule less.hyps [of "s'"])
-        using True d  `finite s` not_in_interior_convex_hull_3
+        using True d  \<open>finite s\<close> not_in_interior_convex_hull_3
         apply (auto intro!: less.prems continuous_on_subset [OF  _ *])
         apply (metis * insert_absorb insert_subset interior_mono)
         done
@@ -2428,7 +2428,7 @@
         by (meson True hull_subset insert_subset convex_hull_subset)
       have bcd: "(f has_path_integral 0) (linepath b c +++ linepath c d +++ linepath d b)"
         apply (rule less.hyps [of "s'"])
-        using True d  `finite s` not_in_interior_convex_hull_3
+        using True d  \<open>finite s\<close> not_in_interior_convex_hull_3
         apply (auto intro!: less.prems continuous_on_subset [OF _ *])
         apply (metis * insert_absorb insert_subset interior_mono)
         done
@@ -2436,7 +2436,7 @@
         by (meson True hull_subset insert_subset convex_hull_subset)
       have cad: "(f has_path_integral 0) (linepath c a +++ linepath a d +++ linepath d c)"
         apply (rule less.hyps [of "s'"])
-        using True d  `finite s` not_in_interior_convex_hull_3
+        using True d  \<open>finite s\<close> not_in_interior_convex_hull_3
         apply (auto intro!: less.prems continuous_on_subset [OF _ *])
         apply (metis * insert_absorb insert_subset interior_mono)
         done
@@ -2518,7 +2518,7 @@
     then obtain d1 where d1: "d1>0" and d1_less: "\<And>y. cmod (y - x) < d1 \<Longrightarrow> cmod (f y - f x) < e/2"
       unfolding continuous_at Lim_at dist_norm  using e
       by (drule_tac x="e/2" in spec) force
-    obtain d2 where d2: "d2>0" "ball x d2 \<subseteq> s" using  `open s` x
+    obtain d2 where d2: "d2>0" "ball x d2 \<subseteq> s" using  \<open>open s\<close> x
       by (auto simp: open_contains_ball)
     have dpos: "min d1 d2 > 0" using d1 d2 by simp
     { fix y
@@ -2556,7 +2556,7 @@
     apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right)
     apply (rule Lim_transform [OF * Lim_eventually])
     apply (simp add: inverse_eq_divide [symmetric] eventually_at)
-    using `open s` x
+    using \<open>open s\<close> x
     apply (force simp: dist_norm open_contains_ball)
     done
 qed
@@ -2802,7 +2802,7 @@
 proof -
   { fix z
     assume z: "z \<in> s"
-    obtain d where d: "d>0" "ball z d \<subseteq> s" using  `open s` z
+    obtain d where d: "d>0" "ball z d \<subseteq> s" using  \<open>open s\<close> z
       by (auto simp: open_contains_ball)
     then have contfb: "continuous_on (ball z d) f"
       using contf continuous_on_subset by blast
@@ -2839,16 +2839,16 @@
 apply (auto simp: holomorphic_on_open open_delete intro!: derivative_eq_intros)
 done
 
-text{*Key fact that path integral is the same for a "nearby" path. This is the
+text\<open>Key fact that path integral is the same for a "nearby" path. This is the
  main lemma for the homotopy form of Cauchy's theorem and is also useful
  if we want "without loss of generality" to assume some nice properties of a
  path (e.g. smoothness). It can also be used to define the integrals of
  analytic functions over arbitrary continuous paths. This is just done for
  winding numbers now.
-*}
+\<close>
 
-text{*This formulation covers two cases: @{term g} and @{term h} share their
-      start and end points; @{term g} and @{term h} both loop upon themselves. *}
+text\<open>This formulation covers two cases: @{term g} and @{term h} share their
+      start and end points; @{term g} and @{term h} both loop upon themselves.\<close>
 lemma path_integral_nearby:
   assumes os: "open s"
       and p: "path p" "path_image p \<subseteq> s"
@@ -2876,7 +2876,7 @@
     by blast
   then obtain k where k: "k \<subseteq> {0..1}" "finite k" and D_eq: "D = ((\<lambda>z. ball z (ee z / 3)) \<circ> p) ` k"
     apply (simp add: cover_def path_image_def image_comp)
-    apply (blast dest!: finite_subset_image [OF `finite D`])
+    apply (blast dest!: finite_subset_image [OF \<open>finite D\<close>])
     done
   then have kne: "k \<noteq> {}"
     using D by auto
@@ -2905,7 +2905,7 @@
     { fix t::real
       assume t: "0 \<le> t" "t \<le> 1"
       then obtain u where u: "u \<in> k" and ptu: "p t \<in> ball(p u) (ee(p u) / 3)"
-        using `path_image p \<subseteq> \<Union>D` D_eq by (force simp: path_image_def)
+        using \<open>path_image p \<subseteq> \<Union>D\<close> D_eq by (force simp: path_image_def)
       then have ele: "e \<le> ee (p u)" using fin_eep
         by (simp add: e_def)
       have "cmod (g t - p t) < e / 3" "cmod (h t - p t) < e / 3"
@@ -2950,7 +2950,7 @@
         next
           case (Suc n)
           obtain t where t: "t \<in> k" and "p (n/N) \<in> ball(p t) (ee(p t) / 3)"
-            using `path_image p \<subseteq> \<Union>D` [THEN subsetD, where c="p (n/N)"] D_eq N Suc.prems
+            using \<open>path_image p \<subseteq> \<Union>D\<close> [THEN subsetD, where c="p (n/N)"] D_eq N Suc.prems
             by (force simp: path_image_def)
           then have ptu: "cmod (p t - p (n/N)) < ee (p t) / 3"
             by (simp add: dist_norm)
@@ -2988,7 +2988,7 @@
             using ptgh_ee [of "n/N"] Suc.prems
             by (auto simp: field_simps real_of_nat_def dist_norm dest: segment_furthest_le [where y="p t"])
           then have gh_ns: "closed_segment (g (n/N)) (h (n/N)) \<subseteq> s"
-            using `N>0` Suc.prems
+            using \<open>N>0\<close> Suc.prems
             apply (simp add: real_of_nat_def path_image_join field_simps closed_segment_commute)
             apply (erule order_trans)
             apply (simp add: ee pi t)
@@ -2998,14 +2998,14 @@
             using ptgh_ee [of "(1+n)/N"] Suc.prems
             by (auto simp: field_simps real_of_nat_def dist_norm dest: segment_furthest_le [where y="p t"])
           then have gh_n's: "closed_segment (g ((1 + n) / N)) (h ((1 + n) / N)) \<subseteq> s"
-            using `N>0` Suc.prems ee pi t
+            using \<open>N>0\<close> Suc.prems ee pi t
             by (auto simp: Path_Connected.path_image_join field_simps)
           have pi_subset_ball:
                 "path_image (subpath (n/N) ((1+n) / N) g +++ linepath (g ((1+n) / N)) (h ((1+n) / N)) +++
                              subpath ((1+n) / N) (n/N) h +++ linepath (h (n/N)) (g (n/N)))
                  \<subseteq> ball (p t) (ee (p t))"
             apply (intro subset_path_image_join pi_hgn pi_ghn')
-            using `N>0` Suc.prems
+            using \<open>N>0\<close> Suc.prems
             apply (auto simp: dist_norm field_simps closed_segment_eq_real_ivl ptgh_ee)
             done
           have pi0: "(f has_path_integral 0)
@@ -3126,7 +3126,7 @@
   where d: "0 < d"
     and p: "polynomial_function p" "path_image p \<subseteq> s"
     and pi: "\<And>f. f holomorphic_on s \<Longrightarrow> path_integral g f = path_integral p f"
-  using path_integral_nearby_ends [OF s `path g` pag]
+  using path_integral_nearby_ends [OF s \<open>path g\<close> pag]
   apply clarify
   apply (drule_tac x=g in spec)
   apply (simp only: assms)
diff -r bf194f7c4c8e -r 05d28dc76e5c src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Sep 21 21:43:09 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Sep 21 21:46:14 2015 +0200
@@ -9467,7 +9467,7 @@
     using g by (simp add: Fun.image_comp)
   then show "coplanar s"
     unfolding coplanar_def
-    using affine_hull_linear_image [of g "{u,v,w}" for u v w]  `linear g` linear_conv_bounded_linear
+    using affine_hull_linear_image [of g "{u,v,w}" for u v w]  \<open>linear g\<close> linear_conv_bounded_linear
     by fastforce
 qed
 (*The HOL Light proof is simply
@@ -9651,7 +9651,7 @@
     then have *: "\<And>x. x \<in> closure s \<Longrightarrow> setdist s t \<le> dist x y"
       apply (rule continuous_ge_on_closure)
       apply assumption
-      apply (blast intro: setdist_le_dist `y \<in> t` )
+      apply (blast intro: setdist_le_dist \<open>y \<in> t\<close> )
       done
   } note * = this
   show ?thesis
@@ -9687,7 +9687,7 @@
   assumes s: "closed s" and t: "compact t"
       and "s \<noteq> {}" "t \<noteq> {}"
     shows "\<exists>x \<in> s. \<exists>y \<in> t. dist x y = setdist s t"
-  using setdist_compact_closed [OF t s `t \<noteq> {}` `s \<noteq> {}`]
+  using setdist_compact_closed [OF t s \<open>t \<noteq> {}\<close> \<open>s \<noteq> {}\<close>]
   by (metis dist_commute setdist_sym)
 
 lemma setdist_eq_0I: "\<lbrakk>x \<in> s; x \<in> t\<rbrakk> \<Longrightarrow> setdist s t = 0"
diff -r bf194f7c4c8e -r 05d28dc76e5c src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Sep 21 21:43:09 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Sep 21 21:46:14 2015 +0200
@@ -2889,7 +2889,7 @@
         apply (rule less_trans[OF _ *])
         apply (subst N1', rule d(2)[of "p (N1+N2)"])
         using N1' as(1) as(2) dp
-        apply (simp add: `\<forall>x. p x tagged_division_of cbox a b \<and> (\<lambda>xa. \<Inter>{d i xa |i. i \<in> {0..x}}) fine p x`)
+        apply (simp add: \<open>\<forall>x. p x tagged_division_of cbox a b \<and> (\<lambda>xa. \<Inter>{d i xa |i. i \<in> {0..x}}) fine p x\<close>)
         using N2 le_add2 by blast
     }
     ultimately show "\<exists>d. gauge d \<and>
@@ -3602,11 +3602,11 @@
   proof (cases "f x = neutral opp")
     case True
     then show ?thesis
-      using assms `x \<notin> s`
+      using assms \<open>x \<notin> s\<close>
       by (auto simp: iterate_def support_clauses)
   next
     case False
-    with `x \<notin> s` \<open>finite s\<close> support_subset show ?thesis
+    with \<open>x \<notin> s\<close> \<open>finite s\<close> support_subset show ?thesis
       apply (simp add: iterate_def fold'_def support_clauses)
       apply (subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def])
       apply (force simp add: )+
@@ -3962,7 +3962,7 @@
       case True
       show "iterate opp d f = f (cbox a b)"
         unfolding operativeD(1)[OF assms(2) True]
-      proof (rule iterate_eq_neutral[OF `monoidal opp`])
+      proof (rule iterate_eq_neutral[OF \<open>monoidal opp\<close>])
         fix x
         assume x: "x \<in> d"
         then show "f x = neutral opp"
@@ -3990,9 +3990,9 @@
           note *[OF this(1)] *[OF this(2)] note this[unfolded interval_bounds[OF uv(1)]]
           moreover
           have "a\<bullet>j \<le> u\<bullet>j" "v\<bullet>j \<le> b\<bullet>j"
-            using division_ofD(2,2,3)[OF `d division_of cbox a b` as]
+            using division_ofD(2,2,3)[OF \<open>d division_of cbox a b\<close> as]
             apply (metis j subset_box(1) uv(1))
-            by (metis `cbox u v \<subseteq> cbox a b` j subset_box(1) uv(1))
+            by (metis \<open>cbox u v \<subseteq> cbox a b\<close> j subset_box(1) uv(1))
           ultimately have "u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = a\<bullet>j \<or> u\<bullet>j = b\<bullet>j \<and> v\<bullet>j = b\<bullet>j \<or> u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = b\<bullet>j"
             unfolding not_less de_Morgan_disj using ab[rule_format,of j] uv(2) j by force }
         then have d': "\<forall>i\<in>d. \<exists>u v. i = cbox u v \<and>
@@ -4001,7 +4001,7 @@
           by blast
         have "(1/2) *\<^sub>R (a+b) \<in> cbox a b"
           unfolding mem_box using ab by(auto intro!: less_imp_le simp: inner_simps)
-        note this[unfolded division_ofD(6)[OF `d division_of cbox a b`,symmetric] Union_iff]
+        note this[unfolded division_ofD(6)[OF \<open>d division_of cbox a b\<close>,symmetric] Union_iff]
         then guess i .. note i=this
         guess u v using d'[rule_format,OF i(1)] by (elim exE conjE) note uv=this
         have "cbox a b \<in> d"
@@ -4059,18 +4059,18 @@
         def d2 \<equiv> "{l \<inter> {x. x\<bullet>k \<ge> c} | l. l \<in> d \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
         def cb \<equiv> "(\<Sum>i\<in>Basis. (if i = k then c else b\<bullet>i) *\<^sub>R i)::'a"
         def ca \<equiv> "(\<Sum>i\<in>Basis. (if i = k then c else a\<bullet>i) *\<^sub>R i)::'a"
-        note division_points_psubset[OF `d division_of cbox a b` ab kc(1-2) j]
+        note division_points_psubset[OF \<open>d division_of cbox a b\<close> ab kc(1-2) j]
         note psubset_card_mono[OF _ this(1)] psubset_card_mono[OF _ this(2)]
         then have *: "(iterate opp d1 f) = f (cbox a b \<inter> {x. x\<bullet>k \<le> c})"
           "(iterate opp d2 f) = f (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
           unfolding interval_split[OF kc(4)]
           apply (rule_tac[!] "1.hyps"[rule_format])
-          using division_split[OF `d division_of cbox a b`, where k=k and c=c]
-          apply (simp_all add: interval_split 1 kc d1_def d2_def division_points_finite[OF `d division_of cbox a b`])
+          using division_split[OF \<open>d division_of cbox a b\<close>, where k=k and c=c]
+          apply (simp_all add: interval_split 1 kc d1_def d2_def division_points_finite[OF \<open>d division_of cbox a b\<close>])
           done
         { fix l y
           assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} = y \<inter> {x. x \<bullet> k \<le> c}" "l \<noteq> y"
-          from division_ofD(4)[OF `d division_of cbox a b` this(1)] guess u v by (elim exE) note leq=this
+          from division_ofD(4)[OF \<open>d division_of cbox a b\<close> this(1)] guess u v by (elim exE) note leq=this
           have "f (l \<inter> {x. x \<bullet> k \<le> c}) = neutral opp"
             unfolding leq interval_split[OF kc(4)]
             apply (rule operativeD(1) 1)+
@@ -4079,7 +4079,7 @@
         } note fxk_le = this
         { fix l y
           assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} = y \<inter> {x. c \<le> x \<bullet> k}" "l \<noteq> y"
-          from division_ofD(4)[OF `d division_of cbox a b` this(1)] guess u v by (elim exE) note leq=this
+          from division_ofD(4)[OF \<open>d division_of cbox a b\<close> this(1)] guess u v by (elim exE) note leq=this
           have "f (l \<inter> {x. x \<bullet> k \<ge> c}) = neutral opp"
             unfolding leq interval_split[OF kc(4)]
             apply (rule operativeD(1) 1)+
@@ -4102,7 +4102,7 @@
           apply (force simp add: empty_as_interval[symmetric] fxk_ge)+
           done
         also have *: "\<forall>x\<in>d. f x = opp (f (x \<inter> {x. x \<bullet> k \<le> c})) (f (x \<inter> {x. c \<le> x \<bullet> k}))"
-          unfolding forall_in_division[OF `d division_of cbox a b`]
+          unfolding forall_in_division[OF \<open>d division_of cbox a b\<close>]
           using assms(2) kc(4) by blast
         have "opp (iterate opp d (\<lambda>l. f (l \<inter> {x. x \<bullet> k \<le> c}))) (iterate opp d (\<lambda>l. f (l \<inter> {x. c \<le> x \<bullet> k}))) =
           iterate opp d f"
@@ -4689,7 +4689,7 @@
 proof (cases "content (cbox a b) = 0")
   case True
   then have ce: "content (cbox a b) < e"
-    by (metis `0 < e`)
+    by (metis \<open>0 < e\<close>)
   show ?thesis
     apply (rule that[of 1])
     apply simp
@@ -6112,10 +6112,10 @@
   have one: "(- 1) ^ p' * (- 1) ^ p' = (1::real)"
     and "{..<p} \<inter> {i. p = Suc i} = {p - 1}"
     for p'
-    using `p > 0`
+    using \<open>p > 0\<close>
     by (auto simp: power_mult_distrib[symmetric])
   then have "?sum b = f b"
-    using Suc_pred'[OF `p > 0`]
+    using Suc_pred'[OF \<open>p > 0\<close>]
     by (simp add: diff_eq_eq Dg_def power_0_left le_Suc_eq if_distrib
         cond_application_beta setsum.If_cases f0)
   also
@@ -6428,7 +6428,7 @@
   { fix e::real 
     assume "e > 0"
     obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {a..b}; \<bar>x' - x\<bar> < d\<rbrakk> \<Longrightarrow> norm(f x' - f x) \<le> e"
-      using `e>0` fx by (auto simp: continuous_within_eps_delta dist_norm less_imp_le)
+      using \<open>e>0\<close> fx by (auto simp: continuous_within_eps_delta dist_norm less_imp_le)
     have "norm (integral {a..y} f - integral {a..x} f - (y - x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
            if y: "y \<in> {a..b}" and yx: "\<bar>y - x\<bar> < d" for y  
     proof (cases "y < x")
@@ -6447,7 +6447,7 @@
         using False
         apply (simp add: abs_eq_content del: content_real_if)
         apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
-        using yx False d x y `e>0` apply (auto simp add: Idiff fux_int)
+        using yx False d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
         done
     next
       case True
@@ -6465,13 +6465,13 @@
         using True
         apply (simp add: abs_eq_content del: content_real_if)
         apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
-        using yx True d x y `e>0` apply (auto simp add: Idiff fux_int)
+        using yx True d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
         done
       then show ?thesis
         by (simp add: algebra_simps norm_minus_commute)
     qed
     then have "\<exists>d>0. \<forall>y\<in>{a..b}. \<bar>y - x\<bar> < d \<longrightarrow> norm (integral {a..y} f - integral {a..x} f - (y - x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
-      using `d>0` by blast 
+      using \<open>d>0\<close> by blast 
   } 
   then show ?thesis
     by (simp add: has_vector_derivative_def has_derivative_within_alt bounded_linear_scaleR_left)
@@ -11913,7 +11913,7 @@
     by simp
 qed
 
-subsection{*Compute a double integral using iterated integrals and switching the order of integration*}
+subsection\<open>Compute a double integral using iterated integrals and switching the order of integration\<close>
 
 lemma setcomp_dot1: "{z. P (z \<bullet> (i,0))} = {(x,y). P(x \<bullet> i)}"
   by auto
@@ -12197,7 +12197,7 @@
       using compact_uniformly_continuous [OF assms compact_cbox]
       apply (simp add: uniformly_continuous_on_def dist_norm)
       apply (drule_tac x="e / 2 / content?CBOX" in spec)
-      using cbp `0 < e`
+      using cbp \<open>0 < e\<close>
       apply (auto simp: zero_less_mult_iff)
       apply (rename_tac k)
       apply (rule_tac e1=k in fine_division_exists [OF gauge_ball, where a = "(a,c)" and b = "(b,d)"])
diff -r bf194f7c4c8e -r 05d28dc76e5c src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Sep 21 21:43:09 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Sep 21 21:46:14 2015 +0200
@@ -462,7 +462,7 @@
   apply auto
   done
 
-lemma approachable_lt_le2:  --{*like the above, but pushes aside an extra formula*}
+lemma approachable_lt_le2:  --\<open>like the above, but pushes aside an extra formula\<close>
     "(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)"
   apply auto
   apply (rule_tac x="d/2" in exI, auto)
@@ -562,7 +562,7 @@
   using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
   by (auto simp add: field_simps cong: conj_cong)
 
-text{*Bernoulli's inequality*}
+text\<open>Bernoulli's inequality\<close>
 lemma Bernoulli_inequality:
   fixes x :: real
   assumes "-1 \<le> x"
diff -r bf194f7c4c8e -r 05d28dc76e5c src/HOL/Multivariate_Analysis/Uniform_Limit.thy
--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Mon Sep 21 21:43:09 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Mon Sep 21 21:46:14 2015 +0200
@@ -58,15 +58,15 @@
   def e' \<equiv> "e/3"
   assume "0 < e"
   then have "0 < e'" by (simp add: e'_def)
-  from uniform_limitD[OF uc `0 < e'`]
+  from uniform_limitD[OF uc \<open>0 < e'\<close>]
   have "\<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (h x) (f n x) < e'"
     by (simp add: dist_commute)
   moreover
   from f
   have "\<forall>\<^sub>F n in F. \<forall>\<^sub>F x in at x within S. dist (g n) (f n x) < e'"
-    by eventually_elim (auto dest!: tendstoD[OF _ `0 < e'`] simp: dist_commute)
+    by eventually_elim (auto dest!: tendstoD[OF _ \<open>0 < e'\<close>] simp: dist_commute)
   moreover
-  from tendstoD[OF g `0 < e'`] have "\<forall>\<^sub>F x in F. dist l (g x) < e'"
+  from tendstoD[OF g \<open>0 < e'\<close>] have "\<forall>\<^sub>F x in F. dist l (g x) < e'"
     by (simp add: dist_commute)
   ultimately
   have "\<forall>\<^sub>F _ in F. \<forall>\<^sub>F x in at x within S. dist (h x) l < e"
@@ -80,7 +80,7 @@
     show ?case
     proof eventually_elim
       case (elim x)
-      from fh[rule_format, OF `x \<in> S`] elim(1)
+      from fh[rule_format, OF \<open>x \<in> S\<close>] elim(1)
       have "dist (h x) (g n) < e' + e'"
         by (rule dist_triangle_lt[OF add_strict_mono])
       from dist_triangle_lt[OF add_strict_mono, OF this gl]
@@ -88,7 +88,7 @@
     qed
   qed
   thus "\<forall>\<^sub>F x in at x within S. dist (h x) l < e"
-    using eventually_happens by (metis `\<not>trivial_limit F`)
+    using eventually_happens by (metis \<open>\<not>trivial_limit F\<close>)
 qed
 
 lemma
@@ -122,7 +122,7 @@
 proof (rule uniform_limitI)
   fix e :: real
   assume "0 < e"
-  from suminf_exist_split[OF `0 < e` `summable M`]
+  from suminf_exist_split[OF \<open>0 < e\<close> \<open>summable M\<close>]
   have "\<forall>\<^sub>F k in sequentially. norm (\<Sum>i. M (i + k)) < e"
     by (auto simp: eventually_sequentially)
   thus "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>A. dist (\<Sum>i<n. f i x) (\<Sum>i. f i x) < e"
@@ -132,16 +132,16 @@
     proof safe
       fix x assume "x \<in> A"
       have "\<exists>N. \<forall>n\<ge>N. norm (f n x) \<le> M n"
-        using assms(1)[OF `x \<in> A`] by simp
+        using assms(1)[OF \<open>x \<in> A\<close>] by simp
       hence summable_norm_f: "summable (\<lambda>n. norm (f n x))"
-        by(rule summable_norm_comparison_test[OF _ `summable M`])
+        by(rule summable_norm_comparison_test[OF _ \<open>summable M\<close>])
       have summable_f: "summable (\<lambda>n. f n x)"
         using summable_norm_cancel[OF summable_norm_f] .
       have summable_norm_f_plus_k: "summable (\<lambda>i. norm (f (i + k) x))"
         using summable_ignore_initial_segment[OF summable_norm_f]
         by auto
       have summable_M_plus_k: "summable (\<lambda>i. M (i + k))"
-        using summable_ignore_initial_segment[OF `summable M`]
+        using summable_ignore_initial_segment[OF \<open>summable M\<close>]
         by auto
 
       have "dist (\<Sum>i<k. f i x) (\<Sum>i. f i x) = norm ((\<Sum>i. f i x) - (\<Sum>i<k. f i x))"
@@ -152,7 +152,7 @@
         using summable_norm[OF summable_norm_f_plus_k] .
       also have "... \<le> (\<Sum>i. M (i + k))"
         by (rule suminf_le[OF _ summable_norm_f_plus_k summable_M_plus_k])
-           (simp add: assms(1)[OF `x \<in> A`])
+           (simp add: assms(1)[OF \<open>x \<in> A\<close>])
       finally show "dist (\<Sum>i<k. f i x) (\<Sum>i. f i x) < e"
         using elim by auto
     qed
@@ -163,12 +163,12 @@
   by simp
 
 named_theorems uniform_limit_intros "introduction rules for uniform_limit"
-setup {*
+setup \<open>
   Global_Theory.add_thms_dynamic (@{binding uniform_limit_eq_intros},
     fn context =>
       Named_Theorems.get (Context.proof_of context) @{named_theorems uniform_limit_intros}
       |> map_filter (try (fn thm => @{thm uniform_limit_eq_rhs} OF [thm])))
-*}
+\<close>
 
 lemma (in bounded_linear) uniform_limit[uniform_limit_intros]:
   assumes "uniform_limit X g l F"
@@ -178,7 +178,7 @@
   from pos_bounded obtain K
     where K: "\<And>x y. dist (f x) (f y) \<le> K * dist x y" "K > 0"
     by (auto simp: ac_simps dist_norm diff[symmetric])
-  assume "0 < e" with `K > 0` have "e / K > 0" by simp
+  assume "0 < e" with \<open>K > 0\<close> have "e / K > 0" by simp
   from uniform_limitD[OF assms this]
   show "\<forall>\<^sub>F n in F. \<forall>x\<in>X. dist (f (g n x)) (f (l x)) < e"
     by eventually_elim (metis le_less_trans mult.commute pos_less_divide_eq K)
@@ -245,15 +245,15 @@
     and Kl: "Kl > 0" "\<And>x. x \<in> X \<Longrightarrow> norm (l x) \<le> Kl"
     by (auto simp: bounded_pos)
   hence "K * Km * 4 > 0" "K * Kl * 4 > 0"
-    using `K > 0`
+    using \<open>K > 0\<close>
     by simp_all
   assume "0 < e"
 
   hence "sqrt e > 0" by simp
-  from uniform_limitD[OF assms(1) divide_pos_pos[OF this `sqrt (K*4) > 0`]]
-    uniform_limitD[OF assms(2) divide_pos_pos[OF this `sqrt (K*4) > 0`]]
-    uniform_limitD[OF assms(1) divide_pos_pos[OF `e > 0` `K * Km * 4 > 0`]]
-    uniform_limitD[OF assms(2) divide_pos_pos[OF `e > 0` `K * Kl * 4 > 0`]]
+  from uniform_limitD[OF assms(1) divide_pos_pos[OF this \<open>sqrt (K*4) > 0\<close>]]
+    uniform_limitD[OF assms(2) divide_pos_pos[OF this \<open>sqrt (K*4) > 0\<close>]]
+    uniform_limitD[OF assms(1) divide_pos_pos[OF \<open>e > 0\<close> \<open>K * Km * 4 > 0\<close>]]
+    uniform_limitD[OF assms(2) divide_pos_pos[OF \<open>e > 0\<close> \<open>K * Kl * 4 > 0\<close>]]
   show "\<forall>\<^sub>F n in F. \<forall>x\<in>X. dist (prod (f n x) (g n x)) (prod (l x) (m x)) < e"
   proof eventually_elim
     case (elim n)
@@ -266,31 +266,31 @@
         norm (prod (l x) (g n x - m x))"
         by (auto simp: dist_norm prod_diff_prod intro: order_trans norm_triangle_ineq add_mono)
       also note K(2)[of "f n x - l x" "g n x - m x"]
-      also from elim(1)[THEN bspec, OF `_ \<in> X`, unfolded dist_norm]
+      also from elim(1)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
       have "norm (f n x - l x) \<le> sqrt e / sqrt (K * 4)"
         by simp
-      also from elim(2)[THEN bspec, OF `_ \<in> X`, unfolded dist_norm]
+      also from elim(2)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
       have "norm (g n x - m x) \<le> sqrt e / sqrt (K * 4)"
         by simp
       also have "sqrt e / sqrt (K * 4) * (sqrt e / sqrt (K * 4)) * K = e / 4"
-        using `K > 0` `e > 0` by auto
+        using \<open>K > 0\<close> \<open>e > 0\<close> by auto
       also note K(2)[of "f n x - l x" "m x"]
       also note K(2)[of "l x" "g n x - m x"]
-      also from elim(3)[THEN bspec, OF `_ \<in> X`, unfolded dist_norm]
+      also from elim(3)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
       have "norm (f n x - l x) \<le> e / (K * Km * 4)"
         by simp
-      also from elim(4)[THEN bspec, OF `_ \<in> X`, unfolded dist_norm]
+      also from elim(4)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
       have "norm (g n x - m x) \<le> e / (K * Kl * 4)"
         by simp
-      also note Kl(2)[OF `_ \<in> X`]
-      also note Km(2)[OF `_ \<in> X`]
+      also note Kl(2)[OF \<open>_ \<in> X\<close>]
+      also note Km(2)[OF \<open>_ \<in> X\<close>]
       also have "e / (K * Km * 4) * Km * K = e / 4"
-        using `K > 0` `Km > 0` by simp
+        using \<open>K > 0\<close> \<open>Km > 0\<close> by simp
       also have " Kl * (e / (K * Kl * 4)) * K = e / 4"
-        using `K > 0` `Kl > 0` by simp
-      also have "e / 4 + e / 4 + e / 4 < e" using `e > 0` by simp
+        using \<open>K > 0\<close> \<open>Kl > 0\<close> by simp
+      also have "e / 4 + e / 4 + e / 4 < e" using \<open>e > 0\<close> by simp
       finally show "dist (prod (f n x) (g n x)) (prod (l x) (m x)) < e"
-        using `K > 0` `Kl > 0` `Km > 0` `e > 0`
+        using \<open>K > 0\<close> \<open>Kl > 0\<close> \<open>Km > 0\<close> \<open>e > 0\<close>
         by (simp add: algebra_simps mult_right_mono divide_right_mono)
     qed
   qed
diff -r bf194f7c4c8e -r 05d28dc76e5c src/HOL/Multivariate_Analysis/Weierstrass.thy
--- a/src/HOL/Multivariate_Analysis/Weierstrass.thy	Mon Sep 21 21:43:09 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy	Mon Sep 21 21:46:14 2015 +0200
@@ -1,4 +1,4 @@
-section{*Bernstein-Weierstrass and Stone-Weierstrass Theorems*}
+section\<open>Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close>
 
 theory Weierstrass
 imports Uniform_Limit Path_Connected
@@ -11,7 +11,7 @@
 (*Power.thy:*)
 declare power_divide [where b = "numeral w" for w, simp del]
 
-subsection {*Bernstein polynomials*}
+subsection \<open>Bernstein polynomials\<close>
 
 definition Bernstein :: "[nat,nat,real] \<Rightarrow> real" where
   "Bernstein n k x \<equiv> of_nat (n choose k) * x ^ k * (1 - x) ^ (n - k)"
@@ -65,7 +65,7 @@
     by auto
 qed
 
-subsection {*Explicit Bernstein version of the 1D Weierstrass approximation theorem*}
+subsection \<open>Explicit Bernstein version of the 1D Weierstrass approximation theorem\<close>
 
 lemma Bernstein_Weierstrass:
   fixes f :: "real \<Rightarrow> real"
@@ -87,11 +87,11 @@
     assume n: "Suc (nat\<lceil>4*M/(e*d\<^sup>2)\<rceil>) \<le> n" and x: "0 \<le> x" "x \<le> 1"
     have "0 < n" using n by simp
     have ed0: "- (e * d\<^sup>2) < 0"
-      using e `0<d` by simp
+      using e \<open>0<d\<close> by simp
     also have "... \<le> M * 4"
-      using `0\<le>M` by simp
+      using \<open>0\<le>M\<close> by simp
     finally have [simp]: "real (nat \<lceil>4 * M / (e * d\<^sup>2)\<rceil>) = real \<lceil>4 * M / (e * d\<^sup>2)\<rceil>"
-      using `0\<le>M` e `0<d`
+      using \<open>0\<le>M\<close> e \<open>0<d\<close>
       by (simp add: Real.real_of_nat_Suc field_simps)
     have "4*M/(e*d\<^sup>2) + 1 \<le> real (Suc (nat\<lceil>4*M/(e*d\<^sup>2)\<rceil>))"
       by (simp add: Real.real_of_nat_Suc)
@@ -137,7 +137,7 @@
         also have "... \<le> 2 * M * ((x - k/n)\<^sup>2 / d\<^sup>2)"
           apply simp
           apply (rule Rings.ordered_semiring_class.mult_left_mono [of 1 "((x - k/n)\<^sup>2 / d\<^sup>2)", simplified])
-          using dle `d>0` `M\<ge>0` by auto
+          using dle \<open>d>0\<close> \<open>M\<ge>0\<close> by auto
         also have "... \<le> e/2 + 2 * M / d\<^sup>2 * (x - k/n)\<^sup>2"
           using e  by simp
         finally show ?thesis .
@@ -152,12 +152,12 @@
       done
     also have "... \<le> e/2 + (2 * M) / (d\<^sup>2 * n)"
       apply (simp only: setsum.distrib Rings.semiring_class.distrib_right setsum_right_distrib [symmetric] mult.assoc sum_bern)
-      using `d>0` x
+      using \<open>d>0\<close> x
       apply (simp add: divide_simps Mge0 mult_le_one mult_left_le)
       done
     also have "... < e"
       apply (simp add: field_simps)
-      using `d>0` nbig e `n>0`
+      using \<open>d>0\<close> nbig e \<open>n>0\<close>
       apply (simp add: divide_simps algebra_simps)
       using ed0 by linarith
     finally have "\<bar>f x - (\<Sum>k = 0..n. f (real k / real n) * Bernstein n k x)\<bar> < e" .
@@ -167,7 +167,7 @@
 qed
 
 
-subsection {*General Stone-Weierstrass theorem*}
+subsection \<open>General Stone-Weierstrass theorem\<close>
 
 text\<open>Source:
 Bruno Brosowski and Frank Deutsch.
@@ -282,7 +282,7 @@
     show ?thesis
       using subU i t
       apply (clarsimp simp: p_def divide_simps)
-      apply (rule setsum_pos2 [OF `finite subU`])
+      apply (rule setsum_pos2 [OF \<open>finite subU\<close>])
       using Uf t pf01 apply auto
       apply (force elim!: subsetCE)
       done
@@ -345,10 +345,10 @@
     using t0 pf by (simp add: q_def power_0_left)
   { fix t and n::nat
     assume t: "t \<in> s \<inter> V"
-    with `k>0` V have "k * p t < k * \<delta> / 2"
+    with \<open>k>0\<close> V have "k * p t < k * \<delta> / 2"
        by force
     then have "1 - (k * \<delta> / 2)^n \<le> 1 - (k * p t)^n"
-      using  `k>0` p01 t by (simp add: power_mono)
+      using  \<open>k>0\<close> p01 t by (simp add: power_mono)
     also have "... \<le> q n t"
       using Bernoulli_inequality [of "- ((p t)^n)" "k^n"]
       apply (simp add: q_def)
@@ -357,7 +357,7 @@
   } note limitV = this
   { fix t and n::nat
     assume t: "t \<in> s - U"
-    with `k>0` U have "k * \<delta> \<le> k * p t"
+    with \<open>k>0\<close> U have "k * \<delta> \<le> k * p t"
       by (simp add: pt_\<delta>)
     with k\<delta> have kpt: "1 < k * p t"
       by (blast intro: less_le_trans)
@@ -366,9 +366,9 @@
     have ptn_le: "p t ^ n \<le> 1"
       by (meson DiffE atLeastAtMost_iff p01 power_le_one t)
     have "q n t = (1/(k^n * (p t)^n)) * (1 - p t ^ n) ^ (k^n) * k^n * (p t)^n"
-      using pt_pos [OF t] `k>0` by (simp add: q_def)
+      using pt_pos [OF t] \<open>k>0\<close> by (simp add: q_def)
     also have "... \<le> (1/(k * (p t))^n) * (1 - p t ^ n) ^ (k^n) * (1 + k^n * (p t)^n)"
-      using pt_pos [OF t] `k>0`
+      using pt_pos [OF t] \<open>k>0\<close>
       apply simp
       apply (simp only: times_divide_eq_right [symmetric])
       apply (rule mult_left_mono [of "1::real", simplified])
@@ -377,20 +377,20 @@
       using ptn_le by linarith
     also have "... \<le> (1/(k * (p t))^n) * (1 - p t ^ n) ^ (k^n) * (1 + (p t)^n) ^ (k^n)"
       apply (rule mult_left_mono [OF Bernoulli_inequality [of "p t ^ n" "k^n"]])
-      using `k>0` ptn_pos ptn_le
+      using \<open>k>0\<close> ptn_pos ptn_le
       apply (auto simp: power_mult_distrib)
       done
     also have "... = (1/(k * (p t))^n) * (1 - p t ^ (2*n)) ^ (k^n)"
-      using pt_pos [OF t] `k>0`
+      using pt_pos [OF t] \<open>k>0\<close>
       by (simp add: algebra_simps power_mult power2_eq_square power_mult_distrib [symmetric])
     also have "... \<le> (1/(k * (p t))^n) * 1"
       apply (rule mult_left_mono [OF power_le_one])
       apply (metis diff_le_iff(1) less_eq_real_def mult.commute power_le_one power_mult ptn_pos ptn_le)
-      using pt_pos [OF t] `k>0`
+      using pt_pos [OF t] \<open>k>0\<close>
       apply auto
       done
     also have "... \<le> (1 / (k*\<delta>))^n"
-      using `k>0` \<delta>01  power_mono pt_\<delta> t
+      using \<open>k>0\<close> \<delta>01  power_mono pt_\<delta> t
       by (fastforce simp: field_simps)
     finally have "q n t \<le> (1 / (real k * \<delta>)) ^ n " .
   } note limitNonU = this
@@ -401,13 +401,13 @@
   have NN1: "\<And>e. e>0 \<Longrightarrow> (k * \<delta> / 2)^NN e < e"
     apply (subst Transcendental.ln_less_cancel_iff [symmetric])
       prefer 3 apply (subst ln_realpow)
-    using `k>0` `\<delta>>0` NN  k\<delta>
+    using \<open>k>0\<close> \<open>\<delta>>0\<close> NN  k\<delta>
     apply (force simp add: field_simps)+
     done
   have NN0: "\<And>e. e>0 \<Longrightarrow> (1/(k*\<delta>))^NN e < e"
     apply (subst Transcendental.ln_less_cancel_iff [symmetric])
       prefer 3 apply (subst ln_realpow)
-    using `k>0` `\<delta>>0` NN k\<delta>
+    using \<open>k>0\<close> \<open>\<delta>>0\<close> NN k\<delta>
     apply (force simp add: field_simps ln_div)+
     done
   { fix t and e::real
@@ -416,11 +416,11 @@
     proof -
       assume t: "t \<in> s \<inter> V"
       show "1 - q (NN e) t < e"
-        by (metis add.commute diff_le_eq not_le limitV [OF t] less_le_trans [OF NN1 [OF `e>0`]])
+        by (metis add.commute diff_le_eq not_le limitV [OF t] less_le_trans [OF NN1 [OF \<open>e>0\<close>]])
     next
       assume t: "t \<in> s - U"
       show "q (NN e) t < e"
-      using  limitNonU [OF t] less_le_trans [OF NN0 [OF `e>0`]] not_le by blast
+      using  limitNonU [OF t] less_le_trans [OF NN0 [OF \<open>e>0\<close>]] not_le by blast
     qed
   } then have "\<And>e. e > 0 \<Longrightarrow> \<exists>f\<in>R. f ` s \<subseteq> {0..1} \<and> (\<forall>t \<in> s \<inter> V. f t < e) \<and> (\<forall>t \<in> s - U. 1 - e < f t)"
     using q01
@@ -445,7 +445,7 @@
       using assms by auto
     then have "\<exists>V. open V \<and> w \<in> V \<and> s \<inter> V \<subseteq> -B \<and>
                (\<forall>e>0. \<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>x \<in> s \<inter> V. f x < e) \<and> (\<forall>x \<in> s \<inter> B. f x > 1 - e))"
-      using one [of "-B" w b] assms `w \<in> A` by simp
+      using one [of "-B" w b] assms \<open>w \<in> A\<close> by simp
   }
   then obtain Vf where Vf:
          "\<And>w. w \<in> A \<Longrightarrow> open (Vf w) \<and> w \<in> Vf w \<and> s \<inter> Vf w \<subseteq> -B \<and>
@@ -462,7 +462,7 @@
   obtain subA where subA: "subA \<subseteq> A" "finite subA" "A \<subseteq> (\<Union>x \<in> subA. Vf x)"
     by (blast intro: that open_Vf compactE_image [OF com_A _ setsum_max_0])
   then have [simp]: "subA \<noteq> {}"
-    using `a \<in> A` by auto
+    using \<open>a \<in> A\<close> by auto
   then have cardp: "card subA > 0" using subA
     by (simp add: card_gt_0_iff)
   have "\<And>w. w \<in> A \<Longrightarrow> \<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>x \<in> s \<inter> Vf w. f x < e / card subA) \<and> (\<forall>x \<in> s \<inter> B. f x > 1 - e / card subA)"
@@ -623,7 +623,7 @@
     then have fj1: "f t \<le> (j - 1/3)*e"
       by (simp add: A_def)
     then have Anj: "t \<notin> A i" if "i<j" for i
-      using  Aj  `i<j`
+      using  Aj  \<open>i<j\<close>
       apply (simp add: j_def)
       using not_less_Least by blast
     have j1: "1 \<le> j"
@@ -639,7 +639,7 @@
       then obtain d where "i+2+d = j"
         using le_Suc_ex that by blast
       then have "t \<in> B i"
-        using Anj e ge_fx [OF t] `1 \<le> n` fpos [OF t] t
+        using Anj e ge_fx [OF t] \<open>1 \<le> n\<close> fpos [OF t] t
         apply (simp add: A_def B_def)
         apply (clarsimp simp add: field_simps real_of_nat_diff not_le real_of_nat_Suc)
         apply (rule order_trans [of _ "e * 2 + (e * (real d * 3) + e * (real i * 3))"])
@@ -664,9 +664,9 @@
       apply simp
       done
     also have "... \<le> j*e + e*(n - j + 1)*e/n "
-      using `1 \<le> n` e  by (simp add: field_simps)
+      using \<open>1 \<le> n\<close> e  by (simp add: field_simps)
     also have "... \<le> j*e + e*e"
-      using `1 \<le> n` e j1 by (simp add: field_simps)
+      using \<open>1 \<le> n\<close> e j1 by (simp add: field_simps)
     also have "... < (j + 1/3)*e"
       using e by (auto simp: field_simps)
     finally have gj1: "g t < (j + 1 / 3) * e" .
@@ -737,7 +737,7 @@
       assume n: "N \<le> n"  "\<forall>x\<in>s. \<bar>f x - g x\<bar> < 1 / (1 + real n)"
       assume x: "x \<in> s"
       have "\<not> real (Suc n) < inverse e"
-        using `N \<le> n` N using less_imp_inverse_less by force
+        using \<open>N \<le> n\<close> N using less_imp_inverse_less by force
       then have "1 / (1 + real n) \<le> e"
         using e by (simp add: field_simps real_of_nat_Suc)
       then have "\<bar>f x - g x\<bar> < e"
@@ -756,7 +756,7 @@
     done
 qed
 
-text{*A HOL Light formulation*}
+text\<open>A HOL Light formulation\<close>
 corollary Stone_Weierstrass_HOL:
   fixes R :: "('a::t2_space \<Rightarrow> real) set" and s :: "'a set"
   assumes "compact s"  "\<And>c. P(\<lambda>x. c::real)"
@@ -772,12 +772,12 @@
     using assms
     by auto
   show ?thesis
-    using PR.Stone_Weierstrass_basic [OF `continuous_on s f` `0 < e`]
+    using PR.Stone_Weierstrass_basic [OF \<open>continuous_on s f\<close> \<open>0 < e\<close>]
     by blast
 qed
 
 
-subsection {*Polynomial functions*}
+subsection \<open>Polynomial functions\<close>
 
 inductive real_polynomial_function :: "('a::real_normed_vector \<Rightarrow> real) \<Rightarrow> bool" where
     linear: "bounded_linear f \<Longrightarrow> real_polynomial_function f"
@@ -978,7 +978,7 @@
     by (simp add: euclidean_representation_setsum_fun)
 qed
 
-subsection {*Stone-Weierstrass theorem for polynomial functions*}
+subsection \<open>Stone-Weierstrass theorem for polynomial functions\<close>
 
 text\<open>First, we need to show that they are continous, differentiable and separable.\<close>
 
@@ -1048,12 +1048,12 @@
     assume "b \<in> Basis"
     then
     obtain p' where p': "real_polynomial_function p'" and pd: "\<And>x. ((\<lambda>x. p x \<bullet> b) has_real_derivative p' x) (at x)"
-      using assms [unfolded polynomial_function_iff_Basis_inner, rule_format]  `b \<in> Basis`
+      using assms [unfolded polynomial_function_iff_Basis_inner, rule_format]  \<open>b \<in> Basis\<close>
       has_real_derivative_polynomial_function
       by blast
     have "\<exists>q. polynomial_function q \<and> (\<forall>x. ((\<lambda>u. (p u \<bullet> b) *\<^sub>R b) has_vector_derivative q x) (at x))"
       apply (rule_tac x="\<lambda>x. p' x *\<^sub>R b" in exI)
-      using `b \<in> Basis` p'
+      using \<open>b \<in> Basis\<close> p'
       apply (simp add: polynomial_function_iff_Basis_inner inner_Basis)
       apply (auto intro: derivative_eq_intros pd)
       done
@@ -1096,7 +1096,7 @@
     apply (auto intro: real_polynomial_function_separable)
     done
   show ?thesis
-    using PR.Stone_Weierstrass_basic [OF `continuous_on s f` `0 < e`]
+    using PR.Stone_Weierstrass_basic [OF \<open>continuous_on s f\<close> \<open>0 < e\<close>]
     by blast
 qed
 
@@ -1131,7 +1131,7 @@
       by (rule norm_setsum)
     also have "... < of_nat DIM('b) * (e / DIM('b))"
       apply (rule setsum_bounded_above_strict)
-      apply (simp add: Real_Vector_Spaces.scaleR_diff_left [symmetric] pf `x \<in> s`)
+      apply (simp add: Real_Vector_Spaces.scaleR_diff_left [symmetric] pf \<open>x \<in> s\<close>)
       apply (rule DIM_positive)
       done
     also have "... = e"
@@ -1149,8 +1149,8 @@
 
 subsection\<open>Polynomial functions as paths\<close>
 
-text{*One application is to pick a smooth approximation to a path,
-or just pick a smooth path anyway in an open connected set*}
+text\<open>One application is to pick a smooth approximation to a path,
+or just pick a smooth path anyway in an open connected set\<close>
 
 lemma path_polynomial_function:
     fixes g  :: "real \<Rightarrow> 'b::euclidean_space"
@@ -1192,7 +1192,7 @@
 proof -
   have "path_connected s" using assms
     by (simp add: connected_open_path_connected)
-  with `x \<in> s` `y \<in> s` obtain p where p: "path p" "path_image p \<subseteq> s" "pathstart p = x" "pathfinish p = y"
+  with \<open>x \<in> s\<close> \<open>y \<in> s\<close> obtain p where p: "path p" "path_image p \<subseteq> s" "pathstart p = x" "pathfinish p = y"
     by (force simp: path_connected_def)
   have "\<exists>e. 0 < e \<and> (\<forall>x \<in> path_image p. ball x e \<subseteq> s)"
   proof (cases "s = UNIV")
@@ -1211,7 +1211,7 @@
   then obtain e where "0 < e"and eb: "\<And>x. x \<in> path_image p \<Longrightarrow> ball x e \<subseteq> s"
     by auto
   show ?thesis
-    using path_approx_polynomial_function [OF `path p` `0 < e`]
+    using path_approx_polynomial_function [OF \<open>path p\<close> \<open>0 < e\<close>]
     apply clarify
     apply (intro exI conjI, assumption)
     using p