src/HOL/Bit_Operations.thy
changeset 74364 99add5178e51
parent 74309 42523fbf643b
child 74391 930047942f46
--- 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)