src/HOL/Library/Word.thy
changeset 14565 c6dc17aab88a
parent 14494 48ae8d678d88
child 14589 feae7b5fd425
     1.1 --- a/src/HOL/Library/Word.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/HOL/Library/Word.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -260,6 +260,12 @@
     1.4    bitor  :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
     1.5    bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
     1.6  
     1.7 +syntax (HTML output)
     1.8 +  bitnot :: "bit => bit"        ("\<not>\<^sub>b _" [40] 40)
     1.9 +  bitand :: "bit => bit => bit" (infixr "\<and>\<^sub>b" 35)
    1.10 +  bitor  :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
    1.11 +  bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
    1.12 +
    1.13  primrec
    1.14    bitnot_zero: "(bitnot \<zero>) = \<one>"
    1.15    bitnot_one : "(bitnot \<one>)  = \<zero>"