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