src/HOL/Isar_examples/BasicLogic.thy
changeset 7748 5b9c45b21782
parent 7740 2fbe5ce9845f
child 7761 7fab9592384f
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Tue Oct 05 21:20:28 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Wed Oct 06 00:31:40 1999 +0200
     1.3 @@ -5,9 +5,10 @@
     1.4  Basic propositional and quantifier reasoning.
     1.5  *)
     1.6  
     1.7 +header {* Basic reasoning *};
     1.8 +
     1.9  theory BasicLogic = Main:;
    1.10  
    1.11 -
    1.12  subsection {* Some trivialities *};
    1.13  
    1.14  text {* Just a few toy examples to get an idea of how Isabelle/Isar
    1.15 @@ -19,7 +20,6 @@
    1.16    show A; .;
    1.17  qed;
    1.18  
    1.19 -
    1.20  lemma K: "A --> B --> A";
    1.21  proof;
    1.22    assume A;
    1.23 @@ -44,7 +44,6 @@
    1.24  lemma K''': "A --> B --> A";
    1.25    by intro;
    1.26  
    1.27 -
    1.28  lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
    1.29  proof;
    1.30    assume "A --> B --> C";
    1.31 @@ -63,7 +62,6 @@
    1.32    qed;
    1.33  qed;
    1.34  
    1.35 -
    1.36  text {* Variations of backward vs.\ forward reasoning \dots *};
    1.37  
    1.38  lemma "A & B --> B & A";
    1.39 @@ -178,5 +176,4 @@
    1.40    qed;
    1.41  qed;
    1.42  
    1.43 -
    1.44  end;