| changeset 24350 | 4d74f37c6367 |
| parent 24333 | e77ea0ea7f2c |
| child 24353 | 9a7a9b19e925 |
--- a/src/HOL/Word/WordBitwise.thy Mon Aug 20 18:10:13 2007 +0200 +++ b/src/HOL/Word/WordBitwise.thy Mon Aug 20 18:11:09 2007 +0200 @@ -4,6 +4,9 @@ contains theorems to do with bit-wise (logical) operations on words *) + +header {* Bitwise Operations on Words *} + theory WordBitwise imports WordArith begin lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or