| changeset 6892 | 4a905b4a39c8 |
| parent 6881 | 91a2c8b8269a |
| child 7001 | 8121e11ed765 |
--- a/src/HOL/Isar_examples/BasicLogic.thy Sat Jul 03 00:23:17 1999 +0200 +++ b/src/HOL/Isar_examples/BasicLogic.thy Sat Jul 03 00:26:00 1999 +0200 @@ -70,10 +70,10 @@ lemma "A & B --> B & A"; proof; - assume AB: "A & B"; - from AB; have A: A; ..; - from AB; have B: B; ..; - from B A; show "B & A"; ..; + assume ab: "A & B"; + from ab; have a: A; ..; + from ab; have b: B; ..; + from b a; show "B & A"; ..; qed;