src/HOL/Isar_examples/BasicLogic.thy

--- a/src/HOL/Isar_examples/BasicLogic.thy	Wed Oct 06 18:50:40 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Wed Oct 06 18:50:51 1999 +0200
@@ -9,6 +9,7 @@
 
 theory BasicLogic = Main:;
 
+
 subsection {* Some trivialities *};
 
 text {* Just a few toy examples to get an idea of how Isabelle/Isar
@@ -62,7 +63,8 @@
   qed;
 qed;
 
-text {* Variations of backward vs.\ forward reasoning \dots *};
+
+subsection {* Variations of backward vs.\ forward reasoning \dots *};
 
 lemma "A & B --> B & A";
 proof;