intro+;

--- a/src/HOL/Isar_examples/BasicLogic.thy	Tue Aug 17 17:34:18 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Tue Aug 17 17:34:43 1999 +0200
@@ -27,7 +27,7 @@
 qed;
 
 lemma K': "A --> B --> A";
-proof single+   -- {* better use sufficient-to-show here \dots *};
+proof intro+;
   assume A;
   show A; .;
 qed;