# HG changeset patch
# User wenzelm
# Date 934904083 -7200
# Node ID 75cc3a327bd4cbd6f395dce7b456b0f601d06b08
# Parent  6e7b6b8490e0649faa432528b7b50645590a118d
intro+;

diff -r 6e7b6b8490e0 -r 75cc3a327bd4 src/HOL/Isar_examples/BasicLogic.thy
--- 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;