src/HOL/Multivariate_Analysis/Derivative.thy

   qed (insert e, auto)
 qed
 
 text \<open>Hence the following eccentric variant of the inverse function theorem.
   This has no continuity assumptions, but we do need the inverse function.
-  We could put @{text "f' \<circ> g = I"} but this happens to fit with the minimal linear
+  We could put \<open>f' \<circ> g = I\<close> but this happens to fit with the minimal linear
   algebra theory I've set up so far.\<close>
 
 (* move  before left_inverse_linear in Euclidean_Space*)
 
 lemma right_inverse_linear:

   assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s"
   shows   "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)"
 proof -
   from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
     unfolding uniformly_convergent_on_def by blast
-  from x and `open s` have s: "at x within s = at x" by (rule at_within_open)
+  from x and \<open>open s\<close> have s: "at x within s = at x" by (rule at_within_open)
   have "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within s)"
     by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within)
   then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
     "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
   from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
   from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)"
     by (simp add: has_field_derivative_def s)
   have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
-    by (rule has_derivative_transform_within_open[OF `open s` x _ g'])
+    by (rule has_derivative_transform_within_open[OF \<open>open s\<close> x _ g'])
        (insert g, auto simp: sums_iff)
   thus "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)" unfolding differentiable_def
     by (auto simp: summable_def differentiable_def has_field_derivative_def)
 qed
 

   assumes "convex s" "open s"
   assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
   assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
   shows   "(\<lambda>x. \<Sum>n. f n x) differentiable (at x0)"
-  using differentiable_series[OF assms, of x0] `x0 \<in> s` by blast+
+  using differentiable_series[OF assms, of x0] \<open>x0 \<in> s\<close> by blast+
 
 text \<open>Considering derivative @{typ "real \<Rightarrow> 'b::real_normed_vector"} as a vector.\<close>
 
 definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"