--- a/NEWS Sun Sep 26 18:49:55 2021 +0200
+++ b/NEWS Sun Sep 26 20:13:28 2021 +0200
@@ -214,7 +214,7 @@
* Combinator "Fun.swap" resolved into a mere input abbreviation in
separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY.
-* Infix syntax for bit operations AND, OR, XOR is now organized in
+* Infix syntax for bit operations AND, OR, XOR, NOT is now organized in
bundle bit_operations_syntax. INCOMPATIBILITY.
* Bit operations set_bit, unset_bit and flip_bit are now class
--- a/src/HOL/Bit_Operations.thy Sun Sep 26 18:49:55 2021 +0200
+++ b/src/HOL/Bit_Operations.thy Sun Sep 26 20:13:28 2021 +0200
@@ -3509,7 +3509,8 @@
\<close>
no_notation
- "and" (infixr \<open>AND\<close> 64)
+ 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)
@@ -3517,7 +3518,8 @@
begin
notation
- "and" (infixr \<open>AND\<close> 64)
+ 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)