proper latex -- NB: cannot use antiquotation here;

--- a/src/HOL/Word/Bit_Bit.thy	Mon Nov 11 22:00:57 2013 +0100
+++ b/src/HOL/Word/Bit_Bit.thy	Tue Nov 12 11:52:42 2013 +0100
@@ -2,7 +2,7 @@
     Author:     Author: Brian Huffman, PSU and Gerwin Klein, NICTA
 *)
 
-header {* Bit operations in \<Z>\<^sub>2*}
+header {* Bit operations in $\cal Z_2$ *}
 
 theory Bit_Bit
 imports Bit_Operations "~~/src/HOL/Library/Bit"