diff -r ca4e3b75345a -r 5b9c45b21782 src/HOL/Isar_examples/BasicLogic.thy
--- a/src/HOL/Isar_examples/BasicLogic.thy	Tue Oct 05 21:20:28 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Wed Oct 06 00:31:40 1999 +0200
@@ -5,9 +5,10 @@
 Basic propositional and quantifier reasoning.
 *)
 
+header {* Basic reasoning *};
+
 theory BasicLogic = Main:;
 
-
 subsection {* Some trivialities *};
 
 text {* Just a few toy examples to get an idea of how Isabelle/Isar
@@ -19,7 +20,6 @@
   show A; .;
 qed;
 
-
 lemma K: "A --> B --> A";
 proof;
   assume A;
@@ -44,7 +44,6 @@
 lemma K''': "A --> B --> A";
   by intro;
 
-
 lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
 proof;
   assume "A --> B --> C";
@@ -63,7 +62,6 @@
   qed;
 qed;
 
-
 text {* Variations of backward vs.\ forward reasoning \dots *};
 
 lemma "A & B --> B & A";
@@ -178,5 +176,4 @@
   qed;
 qed;
 
-
 end;