Theory Word_Lib.Word_Syntax
section "Additional Syntax for Word Bit Operations"
theory Word_Syntax
imports
"HOL-Library.Word"
begin
text ‹Additional bit and type syntax that forces word types.›
context
includes bit_operations_syntax
begin
abbreviation
wordNOT :: "'a::len word ⇒ 'a word" ("~~ _" [70] 71)
where
"~~ x == NOT x"
abbreviation
wordAND :: "'a::len word ⇒ 'a word ⇒ 'a word" (infixr "&&" 64)
where
"a && b == a AND b"
abbreviation
wordOR :: "'a::len word ⇒ 'a word ⇒ 'a word" (infixr "||" 59)
where
"a || b == a OR b"
abbreviation
wordXOR :: "'a::len word ⇒ 'a word ⇒ 'a word" (infixr "xor" 59)
where
"a xor b == a XOR b"
end
end