--- 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