src/HOL/Isar_examples/BasicLogic.thy
changeset 7133 64c9f2364dae
parent 7005 cc778d613217
child 7233 75cc3a327bd4
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Fri Jul 30 13:43:26 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Fri Jul 30 13:44:29 1999 +0200
     1.3 @@ -145,7 +145,7 @@
     1.4   context again later. *};
     1.5  
     1.6  theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
     1.7 -proof same;
     1.8 +proof -;
     1.9    assume ab: "A & B";
    1.10    assume ab_c: "A ==> B ==> C";
    1.11    show C;