# HG changeset patch
# User wenzelm
# Date 1728396931 -7200
# Node ID dff7dfd8dce371b720d4f515b089a22920eabf0a
# Parent  bad7156a7814e20304c461bb2b7104794d2f7997
more robust declarations via "no syntax" bundles;

diff -r bad7156a7814 -r dff7dfd8dce3 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Tue Oct 08 16:14:36 2024 +0200
+++ b/src/HOL/Bit_Operations.thy	Tue Oct 08 16:15:31 2024 +0200
@@ -3986,21 +3986,15 @@
   \<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
   by (fact bit_push_bit_iff')
 
-no_notation
-  not  (\<open>NOT\<close>)
-    and "and"  (infixr \<open>AND\<close> 64)
-    and or  (infixr \<open>OR\<close>  59)
-    and xor  (infixr \<open>XOR\<close> 59)
-
 bundle bit_operations_syntax
 begin
-
 notation
   not  (\<open>NOT\<close>)
     and "and"  (infixr \<open>AND\<close> 64)
     and or  (infixr \<open>OR\<close>  59)
     and xor  (infixr \<open>XOR\<close> 59)
+end
+
+unbundle no bit_operations_syntax
 
 end
-
-end
diff -r bad7156a7814 -r dff7dfd8dce3 src/HOL/Computational_Algebra/Formal_Laurent_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Tue Oct 08 16:14:36 2024 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Tue Oct 08 16:15:31 2024 +0200
@@ -4601,11 +4601,11 @@
 
 subsection \<open>Notation\<close>
 
-no_notation fls_nth (infixl \<open>$$\<close> 75)
-
 bundle fps_syntax
 begin
 notation fls_nth (infixl \<open>$$\<close> 75)
 end
 
+unbundle no fps_syntax
+
 end
\ No newline at end of file
diff -r bad7156a7814 -r dff7dfd8dce3 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Tue Oct 08 16:14:36 2024 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Tue Oct 08 16:15:31 2024 +0200
@@ -6191,11 +6191,11 @@
 qed
 
 (* TODO: Figure out better notation for this thing *)
-no_notation fps_nth (infixl \<open>$\<close> 75)
-
 bundle fps_syntax
 begin
 notation fps_nth (infixl \<open>$\<close> 75)
 end
 
+unbundle no fps_syntax
+
 end
diff -r bad7156a7814 -r dff7dfd8dce3 src/HOL/Nominal/Examples/Class1.thy
--- a/src/HOL/Nominal/Examples/Class1.thy	Tue Oct 08 16:14:36 2024 +0200
+++ b/src/HOL/Nominal/Examples/Class1.thy	Tue Oct 08 16:15:31 2024 +0200
@@ -8,7 +8,7 @@
 
 text \<open>types\<close>
 
-no_notation not  (\<open>NOT\<close>)
+unbundle no bit_operations_syntax
 
 nominal_datatype ty =
     PR "string"
diff -r bad7156a7814 -r dff7dfd8dce3 src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy	Tue Oct 08 16:14:36 2024 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy	Tue Oct 08 16:15:31 2024 +0200
@@ -12,13 +12,7 @@
 text \<open>We show how other default types help to find counterexamples to propositions if
   the standard default type \<^typ>\<open>int\<close> is insufficient.\<close>
 
-notation
-  less_eq  (infix \<open>\<sqsubseteq>\<close> 50) and
-  less  (infix \<open>\<sqsubset>\<close> 50) and
-  top (\<open>\<top>\<close>) and
-  bot (\<open>\<bottom>\<close>) and
-  inf (infixl \<open>\<sqinter>\<close> 70) and
-  sup (infixl \<open>\<squnion>\<close> 65)
+unbundle lattice_syntax
 
 declare [[quickcheck_narrowing_active = false, quickcheck_timeout = 3600]]
 
@@ -131,13 +125,6 @@
   quickcheck[expect = no_counterexample]
   by (simp add: eq_iff)
 
-
-no_notation
-  less_eq  (infix \<open>\<sqsubseteq>\<close> 50) and
-  less (infix \<open>\<sqsubset>\<close> 50) and
-  inf  (infixl \<open>\<sqinter>\<close> 70) and
-  sup  (infixl \<open>\<squnion>\<close> 65) and
-  top (\<open>\<top>\<close>) and
-  bot (\<open>\<bottom>\<close>)
+unbundle no lattice_syntax
 
 end