# HG changeset patch
# User wenzelm
# Date 1414946212 -3600
# Node ID be4d203d35b3d7ccff54f40a7c2d476ecb37e034
# Parent  fef1df4268d60de9c1d74cd2e5a8f7239eabf28b
modernized header;

diff -r fef1df4268d6 -r be4d203d35b3 src/HOL/Hoare_Parallel/Gar_Coll.thy
--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy	Sun Nov 02 17:27:22 2014 +0100
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy	Sun Nov 02 17:36:52 2014 +0100
@@ -1,4 +1,4 @@
-header {* \section{The Single Mutator Case} *}
+section {* The Single Mutator Case *}
 
 theory Gar_Coll imports Graph OG_Syntax begin
 
diff -r fef1df4268d6 -r be4d203d35b3 src/HOL/Hoare_Parallel/Graph.thy
--- a/src/HOL/Hoare_Parallel/Graph.thy	Sun Nov 02 17:27:22 2014 +0100
+++ b/src/HOL/Hoare_Parallel/Graph.thy	Sun Nov 02 17:36:52 2014 +0100
@@ -1,6 +1,6 @@
-header {* \chapter{Case Study: Single and Multi-Mutator Garbage Collection Algorithms}
+chapter {* Case Study: Single and Multi-Mutator Garbage Collection Algorithms *}
 
-\section {Formalization of the Memory} *}
+section {* Formalization of the Memory *}
 
 theory Graph imports Main begin
 
diff -r fef1df4268d6 -r be4d203d35b3 src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy
--- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Sun Nov 02 17:27:22 2014 +0100
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Sun Nov 02 17:36:52 2014 +0100
@@ -1,5 +1,4 @@
-
-header {* \section{The Multi-Mutator Case} *}
+section {* The Multi-Mutator Case *}
 
 theory Mul_Gar_Coll imports Graph OG_Syntax begin
 
diff -r fef1df4268d6 -r be4d203d35b3 src/HOL/Hoare_Parallel/OG_Com.thy
--- a/src/HOL/Hoare_Parallel/OG_Com.thy	Sun Nov 02 17:27:22 2014 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Com.thy	Sun Nov 02 17:36:52 2014 +0100
@@ -1,7 +1,6 @@
+chapter {* The Owicki-Gries Method *} 
 
-header {* \chapter{The Owicki-Gries Method} 
-
-\section{Abstract Syntax} *} 
+section {* Abstract Syntax *}
 
 theory OG_Com imports Main begin
 
diff -r fef1df4268d6 -r be4d203d35b3 src/HOL/Hoare_Parallel/OG_Examples.thy
--- a/src/HOL/Hoare_Parallel/OG_Examples.thy	Sun Nov 02 17:27:22 2014 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy	Sun Nov 02 17:36:52 2014 +0100
@@ -1,4 +1,4 @@
-header {* \section{Examples} *}
+section {* Examples *}
 
 theory OG_Examples imports OG_Syntax begin
 
diff -r fef1df4268d6 -r be4d203d35b3 src/HOL/Hoare_Parallel/OG_Hoare.thy
--- a/src/HOL/Hoare_Parallel/OG_Hoare.thy	Sun Nov 02 17:27:22 2014 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy	Sun Nov 02 17:36:52 2014 +0100
@@ -1,5 +1,4 @@
-
-header {* \section{The Proof System} *}
+section {* The Proof System *}
 
 theory OG_Hoare imports OG_Tran begin
 
diff -r fef1df4268d6 -r be4d203d35b3 src/HOL/Hoare_Parallel/OG_Tactics.thy
--- a/src/HOL/Hoare_Parallel/OG_Tactics.thy	Sun Nov 02 17:27:22 2014 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Tactics.thy	Sun Nov 02 17:36:52 2014 +0100
@@ -1,4 +1,4 @@
-header {* \section{Generation of Verification Conditions} *}
+section {* Generation of Verification Conditions *}
 
 theory OG_Tactics
 imports OG_Hoare
diff -r fef1df4268d6 -r be4d203d35b3 src/HOL/Hoare_Parallel/OG_Tran.thy
--- a/src/HOL/Hoare_Parallel/OG_Tran.thy	Sun Nov 02 17:27:22 2014 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Tran.thy	Sun Nov 02 17:36:52 2014 +0100
@@ -1,5 +1,4 @@
-
-header {* \section{Operational Semantics} *}
+section {* Operational Semantics *}
 
 theory OG_Tran imports OG_Com begin
 
diff -r fef1df4268d6 -r be4d203d35b3 src/HOL/Hoare_Parallel/Quote_Antiquote.thy
--- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Sun Nov 02 17:27:22 2014 +0100
+++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Sun Nov 02 17:36:52 2014 +0100
@@ -1,5 +1,4 @@
-
-header {* \section{Concrete Syntax} *}
+section {* Concrete Syntax *}
 
 theory Quote_Antiquote imports Main begin
 
diff -r fef1df4268d6 -r be4d203d35b3 src/HOL/Hoare_Parallel/RG_Com.thy
--- a/src/HOL/Hoare_Parallel/RG_Com.thy	Sun Nov 02 17:27:22 2014 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Com.thy	Sun Nov 02 17:36:52 2014 +0100
@@ -1,8 +1,6 @@
-
-header {* \chapter{The Rely-Guarantee Method} 
+chapter {* The Rely-Guarantee Method *}
 
-\section {Abstract Syntax}
-*}
+section {* Abstract Syntax *}
 
 theory RG_Com imports Main begin
 
diff -r fef1df4268d6 -r be4d203d35b3 src/HOL/Hoare_Parallel/RG_Examples.thy
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Sun Nov 02 17:27:22 2014 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Sun Nov 02 17:36:52 2014 +0100
@@ -1,4 +1,4 @@
-header {* \section{Examples} *}
+section {* Examples *}
 
 theory RG_Examples
 imports RG_Syntax
diff -r fef1df4268d6 -r be4d203d35b3 src/HOL/Hoare_Parallel/RG_Hoare.thy
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Sun Nov 02 17:27:22 2014 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Sun Nov 02 17:36:52 2014 +0100
@@ -1,4 +1,4 @@
-header {* \section{The Proof System} *}
+section {* The Proof System *}
 
 theory RG_Hoare imports RG_Tran begin
 
diff -r fef1df4268d6 -r be4d203d35b3 src/HOL/Hoare_Parallel/RG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Sun Nov 02 17:27:22 2014 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Sun Nov 02 17:36:52 2014 +0100
@@ -1,4 +1,4 @@
-header {* \section{Concrete Syntax} *}
+section {* Concrete Syntax *}
 
 theory RG_Syntax
 imports RG_Hoare Quote_Antiquote
diff -r fef1df4268d6 -r be4d203d35b3 src/HOL/Hoare_Parallel/RG_Tran.thy
--- a/src/HOL/Hoare_Parallel/RG_Tran.thy	Sun Nov 02 17:27:22 2014 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Tran.thy	Sun Nov 02 17:36:52 2014 +0100
@@ -1,4 +1,4 @@
-header {* \section{Operational Semantics} *}
+section {* Operational Semantics *}
 
 theory RG_Tran
 imports RG_Com
diff -r fef1df4268d6 -r be4d203d35b3 src/HOL/Hoare_Parallel/document/root.tex
--- a/src/HOL/Hoare_Parallel/document/root.tex	Sun Nov 02 17:27:22 2014 +0100
+++ b/src/HOL/Hoare_Parallel/document/root.tex	Sun Nov 02 17:36:52 2014 +0100
@@ -7,8 +7,6 @@
 \urlstyle{rm}
 \isabellestyle{it}
 
-\renewcommand{\isamarkupheader}[1]{#1}
-
 \begin{document}
 
 \title{Hoare Logic for Parallel Programs}