# HG changeset patch
# User wenzelm
# Date 1661979912 -7200
# Node ID 97b6daab02335cf1557c2d6581ef673133062b60
# Parent  c2812ca1a455c835a6e0d4034b4cd576b06ea23c
eliminated odd Unicode blanks;

diff -r c2812ca1a455 -r 97b6daab0233 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Wed Aug 31 23:00:43 2022 +0200
+++ b/src/HOL/Deriv.thy	Wed Aug 31 23:05:12 2022 +0200
@@ -811,7 +811,7 @@
 lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
   unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff ..
 
-text \<open>due to Christian Pardillo Laursen, replacing a proper epsilon-delta horror\<close>
+text \<open>due to Christian Pardillo Laursen, replacing a proper epsilon-delta horror\<close>
 lemma field_derivative_lim_unique:
   assumes f: "(f has_field_derivative df) (at z)"
     and s: "s \<longlonglongrightarrow> 0"  "\<And>n. s n \<noteq> 0"