(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)
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" (‹(‹open_block notation=‹prefix ~~››~~ _)› [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
¤ Dauer der Verarbeitung: 0.2 Sekunden
¤
*© Formatika GbR, Deutschland
