
diff -r 23db3493478f -r 930047942f46 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Wed Sep 29 09:58:19 2021 +0200
+++ b/src/HOL/Bit_Operations.thy	Wed Sep 29 06:56:39 2021 +0000
@@ -3509,7 +3509,7 @@
 \<close>
 
 no_notation
-  not  (\<open>NOT"\<close>)
+  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)
@@ -3518,7 +3518,7 @@
 begin
 
 notation
-  not  (\<open>NOT"\<close>)
+  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)




