--- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Wed Oct 02 22:08:52 2024 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Wed Oct 02 23:47:07 2024 +0200
@@ -25,7 +25,7 @@
setup_lifting type_definition_fls
-unbundle fps_notation
+unbundle fps_syntax
notation fls_nth (infixl \<open>$$\<close> 75)
lemmas fls_eqI = iffD1[OF fls_nth_inject, OF iffD2, OF fun_eq_iff, OF allI]
@@ -4603,7 +4603,7 @@
no_notation fls_nth (infixl \<open>$$\<close> 75)
-bundle fls_notation
+bundle fps_syntax
begin
notation fls_nth (infixl \<open>$$\<close> 75)
end
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Wed Oct 02 22:08:52 2024 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Wed Oct 02 23:47:07 2024 +0200
@@ -6193,7 +6193,7 @@
(* TODO: Figure out better notation for this thing *)
no_notation fps_nth (infixl \<open>$\<close> 75)
-bundle fps_notation
+bundle fps_syntax
begin
notation fps_nth (infixl \<open>$\<close> 75)
end
--- a/src/HOL/Computational_Algebra/Polynomial_FPS.thy Wed Oct 02 22:08:52 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_FPS.thy Wed Oct 02 23:47:07 2024 +0200
@@ -9,7 +9,7 @@
begin
context
- includes fps_notation
+ includes fps_syntax
begin
definition fps_of_poly where
--- a/src/HOL/Decision_Procs/Approximation.thy Wed Oct 02 22:08:52 2024 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Oct 02 23:47:07 2024 +0200
@@ -1143,7 +1143,7 @@
section "Avoid pollution of name space"
-bundle floatarith_notation
+bundle floatarith_syntax
begin
notation Add (\<open>Add\<close>)
@@ -1167,7 +1167,7 @@
end
-bundle no_floatarith_notation
+bundle no_floatarith_syntax
begin
no_notation Add (\<open>Add\<close>)
--- a/src/HOL/Library/Landau_Symbols.thy Wed Oct 02 22:08:52 2024 +0200
+++ b/src/HOL/Library/Landau_Symbols.thy Wed Oct 02 23:47:07 2024 +0200
@@ -1741,7 +1741,7 @@
abbreviation (input) asymp_equiv_at_top where
"asymp_equiv_at_top f g \<equiv> f \<sim>[at_top] g"
-bundle asymp_equiv_notation
+bundle asymp_equiv_syntax
begin
notation asymp_equiv_at_top (infix \<open>\<sim>\<close> 50)
end
--- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy Wed Oct 02 22:08:52 2024 +0200
+++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy Wed Oct 02 23:47:07 2024 +0200
@@ -1716,7 +1716,7 @@
shows "f \<sim>[at_top] eval_monom (dominant_term_ms_aux xs) basis" (is ?thesis1)
and "eventually (\<lambda>x. sgn (f x) = sgn (fst (dominant_term_ms_aux xs))) at_top" (is ?thesis2)
proof -
- include asymp_equiv_notation
+ include asymp_equiv_syntax
from xs(2,1) obtain xs' C b e basis' where xs':
"trimmed C" "xs = MSLCons (C, e) xs'" "basis = b # basis'"
"is_expansion_aux xs' (\<lambda>x. f x - eval C x * b x powr e) (b # basis')"
--- a/src/HOL/Real_Asymp/Real_Asymp_Examples.thy Wed Oct 02 22:08:52 2024 +0200
+++ b/src/HOL/Real_Asymp/Real_Asymp_Examples.thy Wed Oct 02 23:47:07 2024 +0200
@@ -4,7 +4,7 @@
begin
context
- includes asymp_equiv_notation
+ includes asymp_equiv_syntax
begin
subsection \<open>Dominik Gruntz's examples\<close>