# HG changeset patch
# User haftmann
# Date 1632555927 0
# Node ID 99add5178e51519de89c36f31e87c557b6e87ac7
# Parent  383fd113baaef48b89f6d29f0efd0873d491fc44
NOT is part of syntax bundle also

diff -r 383fd113baae -r 99add5178e51 NEWS
--- 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
diff -r 383fd113baae -r 99add5178e51 src/HOL/Bit_Operations.thy
--- 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)