diff -r 3667b4616e9a -r c6dc17aab88a src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/Library/Word.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -260,6 +260,12 @@
   bitor  :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
   bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
 
+syntax (HTML output)
+  bitnot :: "bit => bit"        ("\<not>\<^sub>b _" [40] 40)
+  bitand :: "bit => bit => bit" (infixr "\<and>\<^sub>b" 35)
+  bitor  :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
+  bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
+
 primrec
   bitnot_zero: "(bitnot \<zero>) = \<one>"
   bitnot_one : "(bitnot \<one>)  = \<zero>"