fixed intro steps;

--- a/src/HOL/Isar_examples/BasicLogic.thy	Wed Dec 05 03:19:14 2001 +0100
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Wed Dec 05 03:19:47 2001 +0100
@@ -113,7 +113,7 @@
 *}
 
 lemma "A --> B --> A"
-proof intro
+proof (intro impI)
   assume A
   show A .
 qed
@@ -123,7 +123,7 @@
 *}
 
 lemma "A --> B --> A"
-  by intro
+  by (intro impI)
 
 text {*
  Just like $\idt{rule}$, the $\idt{intro}$ and $\idt{elim}$ proof