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
```