| changeset 58874 | 7172c7ffb047 |
| parent 55210 | d1e3b708d74b |
| child 61799 | 4cf66f21b764 |
--- a/src/HOL/Word/Bits_Bit.thy Sun Nov 02 16:50:42 2014 +0100 +++ b/src/HOL/Word/Bits_Bit.thy Sun Nov 02 16:54:06 2014 +0100 @@ -2,7 +2,7 @@ Author: Author: Brian Huffman, PSU and Gerwin Klein, NICTA *) -header {* Bit operations in $\cal Z_2$ *} +section {* Bit operations in $\cal Z_2$ *} theory Bits_Bit imports Bits "~~/src/HOL/Library/Bit"