# HG changeset patch
# User wenzelm
# Date 1007518787 -3600
# Node ID fe2353a8d1e891a699fb487c1b3c946fe6aa7d32
# Parent  9c38ec9eca1c6b2289d2f0a2101f861515f25c35
fixed intro steps;

diff -r 9c38ec9eca1c -r fe2353a8d1e8 src/HOL/Isar_examples/BasicLogic.thy
--- 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