--- a/NEWS Fri Sep 24 22:44:13 2021 +0200
+++ b/NEWS Sat Sep 25 07:45:27 2021 +0000
@@ -205,7 +205,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 Fri Sep 24 22:44:13 2021 +0200
+++ b/src/HOL/Bit_Operations.thy Sat Sep 25 07:45:27 2021 +0000
@@ -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)