# HG changeset patch
# User wenzelm
# Date 1727905627 -7200
# Node ID ad5fc948e053b866f9dbf62cefb7a2ed0689cb0a
# Parent  849efff7de153cc3d8fd483d047b179367ecdad7
more standard bundle names;

diff -r 849efff7de15 -r ad5fc948e053 src/HOL/Computational_Algebra/Formal_Laurent_Series.thy
--- 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
diff -r 849efff7de15 -r ad5fc948e053 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- 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
diff -r 849efff7de15 -r ad5fc948e053 src/HOL/Computational_Algebra/Polynomial_FPS.thy
--- 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
diff -r 849efff7de15 -r ad5fc948e053 src/HOL/Decision_Procs/Approximation.thy
--- 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>)
diff -r 849efff7de15 -r ad5fc948e053 src/HOL/Library/Landau_Symbols.thy
--- 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
diff -r 849efff7de15 -r ad5fc948e053 src/HOL/Real_Asymp/Multiseries_Expansion.thy
--- 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')"
diff -r 849efff7de15 -r ad5fc948e053 src/HOL/Real_Asymp/Real_Asymp_Examples.thy
--- 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>