--- a/src/HOL/Analysis/Lipschitz.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy Fri Sep 20 19:51:08 2024 +0200
@@ -13,10 +13,10 @@
where "lipschitz_on C U f \<longleftrightarrow> (0 \<le> C \<and> (\<forall>x \<in> U. \<forall>y\<in>U. dist (f x) (f y) \<le> C * dist x y))"
bundle lipschitz_syntax begin
-notation\<^marker>\<open>tag important\<close> lipschitz_on ("_-lipschitz'_on" [1000])
+notation\<^marker>\<open>tag important\<close> lipschitz_on (\<open>_-lipschitz'_on\<close> [1000])
end
bundle no_lipschitz_syntax begin
-no_notation lipschitz_on ("_-lipschitz'_on" [1000])
+no_notation lipschitz_on (\<open>_-lipschitz'_on\<close> [1000])
end
unbundle lipschitz_syntax