src/HOL/Isar_examples/BasicLogic.thy
 changeset 7604 55566b9ec7d7 parent 7480 0a0e0dbe1269 child 7740 2fbe5ce9845f
```     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Sat Sep 25 13:18:20 1999 +0200
1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Sat Sep 25 13:18:38 1999 +0200
1.3 @@ -8,7 +8,7 @@
1.4  theory BasicLogic = Main:;
1.5
1.6
1.7 -text {* Just a few tiny examples to get an idea of how Isabelle/Isar
1.8 +text {* Just a few toy examples to get an idea of how Isabelle/Isar
1.9    proof documents may look like. *};
1.10
1.11  lemma I: "A --> A";
1.12 @@ -62,7 +62,7 @@
1.13  qed;
1.14
1.15
1.16 -text {* Variations of backward vs.\ forward reasonong \dots *};
1.17 +text {* Variations of backward vs.\ forward reasoning \dots *};
1.18
1.19  lemma "A & B --> B & A";
1.20  proof;
1.21 @@ -86,6 +86,16 @@
1.22
1.23  lemma "A & B --> B & A";
1.24  proof;
1.25 +  assume "A & B";
1.26 +  show "B & A";
1.27 +  proof;
1.28 +    from prems; show B; ..;
1.29 +    from prems; show A; ..;
1.30 +  qed;
1.31 +qed;
1.32 +
1.33 +lemma "A & B --> B & A";
1.34 +proof;
1.35    assume ab: "A & B";
1.36    from ab; have a: A; ..;
1.37    from ab; have b: B; ..;
```