src/HOL/Isar_examples/BasicLogic.thy
changeset 6892 4a905b4a39c8
parent 6881 91a2c8b8269a
child 7001 8121e11ed765
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Sat Jul 03 00:23:17 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Sat Jul 03 00:26:00 1999 +0200
     1.3 @@ -70,10 +70,10 @@
     1.4  
     1.5  lemma "A & B --> B & A";
     1.6  proof;
     1.7 -  assume AB: "A & B";
     1.8 -  from AB; have A: A; ..;
     1.9 -  from AB; have B: B; ..;
    1.10 -  from B A; show "B & A"; ..;
    1.11 +  assume ab: "A & B";
    1.12 +  from ab; have a: A; ..;
    1.13 +  from ab; have b: B; ..;
    1.14 +  from b a; show "B & A"; ..;
    1.15  qed;
    1.16  
    1.17