# HG changeset patch
# User wenzelm
# Date 935156566 -7200
# Node ID cd0533d52e55cfbb89ffa9840ea4ef1041c25410
# Parent  dad3b686941c1edfd34f955715d48a68cecec5ff
intro (no +);

diff -r dad3b686941c -r cd0533d52e55 src/HOL/Isar_examples/BasicLogic.thy
--- 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;