src/HOL/Isar_examples/BasicLogic.thy

--- a/src/HOL/Isar_examples/BasicLogic.thy	Fri Jul 30 13:43:26 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Fri Jul 30 13:44:29 1999 +0200
@@ -145,7 +145,7 @@
  context again later. *};
 
 theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
-proof same;
+proof -;
   assume ab: "A & B";
   assume ab_c: "A ==> B ==> C";
   show C;