--- a/src/HOL/Isar_examples/BasicLogic.thy Fri Aug 20 15:42:20 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy Fri Aug 20 15:42:46 1999 +0200
@@ -27,7 +27,7 @@
qed;
lemma K': "A --> B --> A";
-proof intro+;
+proof intro;
assume A;
show A; .;
qed;