src/HOL/Isar_examples/BasicLogic.thy
changeset 7761 7fab9592384f
parent 7748 5b9c45b21782
child 7820 cad7cc30fa40
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Wed Oct 06 18:50:40 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Wed Oct 06 18:50:51 1999 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  
     1.5  theory BasicLogic = Main:;
     1.6  
     1.7 +
     1.8  subsection {* Some trivialities *};
     1.9  
    1.10  text {* Just a few toy examples to get an idea of how Isabelle/Isar
    1.11 @@ -62,7 +63,8 @@
    1.12    qed;
    1.13  qed;
    1.14  
    1.15 -text {* Variations of backward vs.\ forward reasoning \dots *};
    1.16 +
    1.17 +subsection {* Variations of backward vs.\ forward reasoning \dots *};
    1.18  
    1.19  lemma "A & B --> B & A";
    1.20  proof;