Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Word.thy
changeset 14565 c6dc17aab88a
parent 14494 48ae8d678d88
child 14589 feae7b5fd425 
--- 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>"
isabelle