--- a/src/HOL/Isar_Examples/Basic_Logic.thy Sun Nov 02 17:20:45 2014 +0100
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy Sun Nov 02 17:23:48 2014 +0100
@@ -4,7 +4,7 @@
Basic propositional and quantifier reasoning.
*)
-header \<open>Basic logical reasoning\<close>
+section \<open>Basic logical reasoning\<close>
theory Basic_Logic
imports Main
--- a/src/HOL/Isar_Examples/Cantor.thy Sun Nov 02 17:20:45 2014 +0100
+++ b/src/HOL/Isar_Examples/Cantor.thy Sun Nov 02 17:23:48 2014 +0100
@@ -2,7 +2,7 @@
Author: Markus Wenzel, TU Muenchen
*)
-header \<open>Cantor's Theorem\<close>
+section \<open>Cantor's Theorem\<close>
theory Cantor
imports Main
--- a/src/HOL/Isar_Examples/Drinker.thy Sun Nov 02 17:20:45 2014 +0100
+++ b/src/HOL/Isar_Examples/Drinker.thy Sun Nov 02 17:23:48 2014 +0100
@@ -2,7 +2,7 @@
Author: Makarius
*)
-header \<open>The Drinker's Principle\<close>
+section \<open>The Drinker's Principle\<close>
theory Drinker
imports Main
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy Sun Nov 02 17:20:45 2014 +0100
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy Sun Nov 02 17:23:48 2014 +0100
@@ -4,7 +4,7 @@
Correctness of a simple expression/stack-machine compiler.
*)
-header \<open>Correctness of a simple expression compiler\<close>
+section \<open>Correctness of a simple expression compiler\<close>
theory Expr_Compiler
imports Main
--- a/src/HOL/Isar_Examples/Fibonacci.thy Sun Nov 02 17:20:45 2014 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy Sun Nov 02 17:23:48 2014 +0100
@@ -12,7 +12,7 @@
(Addison-Wesley, 1989)
*)
-header \<open>Fib and Gcd commute\<close>
+section \<open>Fib and Gcd commute\<close>
theory Fibonacci
imports "../Number_Theory/Primes"
--- a/src/HOL/Isar_Examples/Group.thy Sun Nov 02 17:20:45 2014 +0100
+++ b/src/HOL/Isar_Examples/Group.thy Sun Nov 02 17:23:48 2014 +0100
@@ -2,7 +2,7 @@
Author: Markus Wenzel, TU Muenchen
*)
-header \<open>Basic group theory\<close>
+section \<open>Basic group theory\<close>
theory Group
imports Main
--- a/src/HOL/Isar_Examples/Group_Context.thy Sun Nov 02 17:20:45 2014 +0100
+++ b/src/HOL/Isar_Examples/Group_Context.thy Sun Nov 02 17:23:48 2014 +0100
@@ -2,7 +2,7 @@
Author: Makarius
*)
-header \<open>Some algebraic identities derived from group axioms -- theory context version\<close>
+section \<open>Some algebraic identities derived from group axioms -- theory context version\<close>
theory Group_Context
imports Main
--- a/src/HOL/Isar_Examples/Group_Notepad.thy Sun Nov 02 17:20:45 2014 +0100
+++ b/src/HOL/Isar_Examples/Group_Notepad.thy Sun Nov 02 17:23:48 2014 +0100
@@ -2,7 +2,7 @@
Author: Makarius
*)
-header \<open>Some algebraic identities derived from group axioms -- proof notepad version\<close>
+section \<open>Some algebraic identities derived from group axioms -- proof notepad version\<close>
theory Group_Notepad
imports Main
--- a/src/HOL/Isar_Examples/Hoare.thy Sun Nov 02 17:20:45 2014 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Sun Nov 02 17:23:48 2014 +0100
@@ -4,7 +4,7 @@
A formulation of Hoare logic suitable for Isar.
*)
-header \<open>Hoare Logic\<close>
+section \<open>Hoare Logic\<close>
theory Hoare
imports Main
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Sun Nov 02 17:20:45 2014 +0100
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Sun Nov 02 17:23:48 2014 +0100
@@ -1,4 +1,4 @@
-header \<open>Using Hoare Logic\<close>
+section \<open>Using Hoare Logic\<close>
theory Hoare_Ex
imports Hoare
--- a/src/HOL/Isar_Examples/Knaster_Tarski.thy Sun Nov 02 17:20:45 2014 +0100
+++ b/src/HOL/Isar_Examples/Knaster_Tarski.thy Sun Nov 02 17:23:48 2014 +0100
@@ -4,7 +4,7 @@
Typical textbook proof example.
*)
-header \<open>Textbook-style reasoning: the Knaster-Tarski Theorem\<close>
+section \<open>Textbook-style reasoning: the Knaster-Tarski Theorem\<close>
theory Knaster_Tarski
imports Main "~~/src/HOL/Library/Lattice_Syntax"
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Sun Nov 02 17:20:45 2014 +0100
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Sun Nov 02 17:23:48 2014 +0100
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory (original scripts)
*)
-header \<open>The Mutilated Checker Board Problem\<close>
+section \<open>The Mutilated Checker Board Problem\<close>
theory Mutilated_Checkerboard
imports Main
--- a/src/HOL/Isar_Examples/Nested_Datatype.thy Sun Nov 02 17:20:45 2014 +0100
+++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Sun Nov 02 17:23:48 2014 +0100
@@ -1,4 +1,4 @@
-header \<open>Nested datatypes\<close>
+section \<open>Nested datatypes\<close>
theory Nested_Datatype
imports Main
--- a/src/HOL/Isar_Examples/Peirce.thy Sun Nov 02 17:20:45 2014 +0100
+++ b/src/HOL/Isar_Examples/Peirce.thy Sun Nov 02 17:23:48 2014 +0100
@@ -2,7 +2,7 @@
Author: Markus Wenzel, TU Muenchen
*)
-header \<open>Peirce's Law\<close>
+section \<open>Peirce's Law\<close>
theory Peirce
imports Main
--- a/src/HOL/Isar_Examples/Puzzle.thy Sun Nov 02 17:20:45 2014 +0100
+++ b/src/HOL/Isar_Examples/Puzzle.thy Sun Nov 02 17:23:48 2014 +0100
@@ -1,4 +1,4 @@
-header \<open>An old chestnut\<close>
+section \<open>An old chestnut\<close>
theory Puzzle
imports Main
--- a/src/HOL/Isar_Examples/Summation.thy Sun Nov 02 17:20:45 2014 +0100
+++ b/src/HOL/Isar_Examples/Summation.thy Sun Nov 02 17:23:48 2014 +0100
@@ -2,7 +2,7 @@
Author: Markus Wenzel
*)
-header \<open>Summing natural numbers\<close>
+section \<open>Summing natural numbers\<close>
theory Summation
imports Main
--- a/src/HOL/Isar_Examples/document/style.tex Sun Nov 02 17:20:45 2014 +0100
+++ b/src/HOL/Isar_Examples/document/style.tex Sun Nov 02 17:23:48 2014 +0100
@@ -4,8 +4,6 @@
\isabellestyle{it}
\usepackage{pdfsetup}\urlstyle{rm}
-\renewcommand{\isamarkupheader}[1]{\section{#1}}
-
\renewcommand{\isacommand}[1]
{\ifthenelse{\equal{sorry}{#1}}{$\;$\dummyproof}
{\ifthenelse{\equal{oops}{#1}}{$\vdots$}{\isakeyword{#1}}}}