src/HOL/Isar_examples/BasicLogic.thy
changeset 7740 2fbe5ce9845f
parent 7604 55566b9ec7d7
child 7748 5b9c45b21782
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Tue Oct 05 18:16:26 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Tue Oct 05 18:16:41 1999 +0200
     1.3 @@ -8,6 +8,8 @@
     1.4  theory BasicLogic = Main:;
     1.5  
     1.6  
     1.7 +subsection {* Some trivialities *};
     1.8 +
     1.9  text {* Just a few toy examples to get an idea of how Isabelle/Isar
    1.10    proof documents may look like. *};
    1.11  
    1.12 @@ -103,9 +105,9 @@
    1.13  qed;
    1.14  
    1.15  
    1.16 -section {* Examples from 'Introduction to Isabelle' *};
    1.17 +subsection {* A few examples from ``Introduction to Isabelle'' *};
    1.18  
    1.19 -text {* 'Propositional proof' *};
    1.20 +subsubsection {* Propositional proof *};
    1.21  
    1.22  lemma "P | P --> P";
    1.23  proof;
    1.24 @@ -125,7 +127,7 @@
    1.25  qed;
    1.26  
    1.27  
    1.28 -text {* 'Quantifier proof' *};
    1.29 +subsubsection {* Quantifier proof *};
    1.30  
    1.31  lemma "(EX x. P(f(x))) --> (EX x. P(x))";
    1.32  proof;
    1.33 @@ -153,7 +155,7 @@
    1.34    by blast;
    1.35  
    1.36  
    1.37 -subsection {* 'Deriving rules in Isabelle' *};
    1.38 +subsubsection {* Deriving rules in Isabelle *};
    1.39  
    1.40  text {* We derive the conjunction elimination rule from the
    1.41   projections.  The proof below follows the basic reasoning of the