# HG changeset patch
# User wenzelm
# Date 1414943646 -3600
# Node ID 7172c7ffb04788dedfd7be011f43d066f9768aa9
# Parent  db866dc081f88e6f5ae582ce55cc8c4dbb0d4ee1
modernized header;

diff -r db866dc081f8 -r 7172c7ffb047 src/HOL/Word/Bit_Representation.thy
--- 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
diff -r db866dc081f8 -r 7172c7ffb047 src/HOL/Word/Bits.thy
--- 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
diff -r db866dc081f8 -r 7172c7ffb047 src/HOL/Word/Bits_Bit.thy
--- 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"
diff -r db866dc081f8 -r 7172c7ffb047 src/HOL/Word/Bits_Int.thy
--- 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
diff -r db866dc081f8 -r 7172c7ffb047 src/HOL/Word/Bool_List_Representation.thy
--- 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
diff -r db866dc081f8 -r 7172c7ffb047 src/HOL/Word/Examples/WordExamples.thy
--- 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"
diff -r db866dc081f8 -r 7172c7ffb047 src/HOL/Word/Misc_Numeric.thy
--- 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
diff -r db866dc081f8 -r 7172c7ffb047 src/HOL/Word/Misc_Typedef.thy
--- 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
diff -r db866dc081f8 -r 7172c7ffb047 src/HOL/Word/Type_Length.thy
--- 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"
diff -r db866dc081f8 -r 7172c7ffb047 src/HOL/Word/Word.thy
--- 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
diff -r db866dc081f8 -r 7172c7ffb047 src/HOL/Word/Word_Miscellaneous.thy
--- 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
diff -r db866dc081f8 -r 7172c7ffb047 src/HOL/Word/document/root.tex
--- 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}