--- a/src/HOL/Analysis/Lipschitz.thy Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy Wed Oct 02 11:27:19 2024 +0200
@@ -12,10 +12,12 @@
definition\<^marker>\<open>tag important\<close> lipschitz_on
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
+bundle lipschitz_syntax
+begin
notation\<^marker>\<open>tag important\<close> lipschitz_on (\<open>_-lipschitz'_on\<close> [1000])
end
-bundle no_lipschitz_syntax begin
+bundle no_lipschitz_syntax
+begin
no_notation lipschitz_on (\<open>_-lipschitz'_on\<close> [1000])
end