--- a/src/HOL/Word/Bit_Representation.thy Sun Nov 02 16:50:42 2014 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Sun Nov 02 16:54:06 2014 +0100
@@ -2,7 +2,7 @@
Author: Jeremy Dawson, NICTA
*)
-header {* Integers as implict bit strings *}
+section {* Integers as implict bit strings *}
theory Bit_Representation
imports Misc_Numeric
--- a/src/HOL/Word/Bits.thy Sun Nov 02 16:50:42 2014 +0100
+++ b/src/HOL/Word/Bits.thy Sun Nov 02 16:54:06 2014 +0100
@@ -2,7 +2,7 @@
Author: Author: Brian Huffman, PSU and Gerwin Klein, NICTA
*)
-header {* Syntactic classes for bitwise operations *}
+section {* Syntactic classes for bitwise operations *}
theory Bits
imports Main
--- 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"
--- a/src/HOL/Word/Bits_Int.thy Sun Nov 02 16:50:42 2014 +0100
+++ b/src/HOL/Word/Bits_Int.thy Sun Nov 02 16:54:06 2014 +0100
@@ -6,7 +6,7 @@
and converting them to and from lists of bools.
*)
-header {* Bitwise Operations on Binary Integers *}
+section {* Bitwise Operations on Binary Integers *}
theory Bits_Int
imports Bits Bit_Representation
--- a/src/HOL/Word/Bool_List_Representation.thy Sun Nov 02 16:50:42 2014 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Sun Nov 02 16:54:06 2014 +0100
@@ -6,7 +6,7 @@
and concatenation.
*)
-header "Bool lists and integers"
+section "Bool lists and integers"
theory Bool_List_Representation
imports Main Bits_Int
--- a/src/HOL/Word/Examples/WordExamples.thy Sun Nov 02 16:50:42 2014 +0100
+++ b/src/HOL/Word/Examples/WordExamples.thy Sun Nov 02 16:54:06 2014 +0100
@@ -4,7 +4,7 @@
Examples demonstrating and testing various word operations.
*)
-header "Examples of word operations"
+section "Examples of word operations"
theory WordExamples
imports "../Word" "../WordBitwise"
--- a/src/HOL/Word/Misc_Numeric.thy Sun Nov 02 16:50:42 2014 +0100
+++ b/src/HOL/Word/Misc_Numeric.thy Sun Nov 02 16:54:06 2014 +0100
@@ -2,7 +2,7 @@
Author: Jeremy Dawson, NICTA
*)
-header {* Useful Numerical Lemmas *}
+section {* Useful Numerical Lemmas *}
theory Misc_Numeric
imports Main
--- a/src/HOL/Word/Misc_Typedef.thy Sun Nov 02 16:50:42 2014 +0100
+++ b/src/HOL/Word/Misc_Typedef.thy Sun Nov 02 16:54:06 2014 +0100
@@ -4,7 +4,7 @@
Consequences of type definition theorems, and of extended type definition.
*)
-header {* Type Definition Theorems *}
+section {* Type Definition Theorems *}
theory Misc_Typedef
imports Main
--- a/src/HOL/Word/Type_Length.thy Sun Nov 02 16:50:42 2014 +0100
+++ b/src/HOL/Word/Type_Length.thy Sun Nov 02 16:54:06 2014 +0100
@@ -2,7 +2,7 @@
Author: John Matthews, Galois Connections, Inc., copyright 2006
*)
-header {* Assigning lengths to types by typeclasses *}
+section {* Assigning lengths to types by typeclasses *}
theory Type_Length
imports "~~/src/HOL/Library/Numeral_Type"
--- a/src/HOL/Word/Word.thy Sun Nov 02 16:50:42 2014 +0100
+++ b/src/HOL/Word/Word.thy Sun Nov 02 16:54:06 2014 +0100
@@ -2,7 +2,7 @@
Author: Jeremy Dawson and Gerwin Klein, NICTA
*)
-header {* A type of finite bit strings *}
+section {* A type of finite bit strings *}
theory Word
imports
--- a/src/HOL/Word/Word_Miscellaneous.thy Sun Nov 02 16:50:42 2014 +0100
+++ b/src/HOL/Word/Word_Miscellaneous.thy Sun Nov 02 16:54:06 2014 +0100
@@ -2,7 +2,7 @@
Author: Miscellaneous
*)
-header {* Miscellaneous lemmas, of at least doubtful value *}
+section {* Miscellaneous lemmas, of at least doubtful value *}
theory Word_Miscellaneous
imports Main "~~/src/HOL/Library/Bit" Misc_Numeric
--- a/src/HOL/Word/document/root.tex Sun Nov 02 16:50:42 2014 +0100
+++ b/src/HOL/Word/document/root.tex Sun Nov 02 16:54:06 2014 +0100
@@ -27,8 +27,7 @@
\newpage
-\renewcommand{\isamarkupheader}[1]%
-{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
+\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
\parindent 0pt\parskip 0.5ex
\input{session}