# HG changeset patch
# User immler
# Date 1566938599 -7200
# Node ID d9a71b41de497a21c28337ced85dd39949f23efb
# Parent  c81ac117afa642cc3f24271ee3f51ed3900a7e6c
fixed typo

diff -r c81ac117afa6 -r d9a71b41de49 src/HOL/Analysis/Lipschitz.thy
--- a/src/HOL/Analysis/Lipschitz.thy	Tue Aug 27 22:41:47 2019 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy	Tue Aug 27 22:43:19 2019 +0200
@@ -367,7 +367,7 @@
 
 We give several variations around this statement. This is essentially a connectedness argument.\<close>
 
-lemma locally_lipschitz_imp_lispchitz_aux:
+lemma locally_lipschitz_imp_lipschitz_aux:
   fixes f::"real \<Rightarrow> ('a::metric_space)"
   assumes "a \<le> b"
           "continuous_on {a..b} f"
@@ -407,7 +407,7 @@
   shows "lipschitz_on M {a..b} f"
 proof (rule lipschitz_onI[OF _ \<open>M \<ge> 0\<close>])
   have *: "dist (f t) (f s) \<le> M * (t-s)" if "s \<le> t" "s \<in> {a..b}" "t \<in> {a..b}" for s t
-  proof (rule locally_lipschitz_imp_lispchitz_aux, simp add: \<open>s \<le> t\<close>)
+  proof (rule locally_lipschitz_imp_lipschitz_aux, simp add: \<open>s \<le> t\<close>)
     show "continuous_on {s..t} f" using continuous_on_subset[OF assms(1)] that by auto
     fix x assume "x \<in> {s..<t}"
     then have "x \<in> {a..<b}" using that by auto