--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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}