# HG changeset patch
# User wenzelm
# Date 1632680008 -7200
# Node ID d1185d02aef5ca0ca86c05b6adfecbe4df837267
# Parent  99add5178e51519de89c36f31e87c557b6e87ac7# Parent  b49bd5d9041f3cb6c5269e4645ed56d3b5aabd40
merged

diff -r b49bd5d9041f -r d1185d02aef5 NEWS
--- 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
diff -r b49bd5d9041f -r d1185d02aef5 src/HOL/Bit_Operations.thy
--- 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)