src/HOL/Isar_examples/BasicLogic.thy

 *)
 
 header {* Basic reasoning *};
 
 theory BasicLogic = Main:;
+
 
 subsection {* Some trivialities *};
 
 text {* Just a few toy examples to get an idea of how Isabelle/Isar
   proof documents may look like. *};

       qed;
     qed;
   qed;
 qed;
 
-text {* Variations of backward vs.\ forward reasoning \dots *};
+
+subsection {* Variations of backward vs.\ forward reasoning \dots *};
 
 lemma "A & B --> B & A";
 proof;
   assume "A & B";
   show "B & A";