| changeset 55210 | d1e3b708d74b |
| parent 54854 | 3324a0078636 |
| child 58874 | 7172c7ffb047 |
| 55209:bfafffd5421d | 55210:d1e3b708d74b |
|---|---|
1 (* Title: HOL/Word/Bit_Bit.thy |
1 (* Title: HOL/Word/Bits_Bit.thy |
2 Author: Author: Brian Huffman, PSU and Gerwin Klein, NICTA |
2 Author: Author: Brian Huffman, PSU and Gerwin Klein, NICTA |
3 *) |
3 *) |
4 |
4 |
5 header {* Bit operations in $\cal Z_2$ *} |
5 header {* Bit operations in $\cal Z_2$ *} |
6 |
6 |