src/HOL/Isar_examples/BasicLogic.thy

--- a/src/HOL/Isar_examples/BasicLogic.thy	Wed Jul 14 13:06:08 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Wed Jul 14 13:07:09 1999 +0200
@@ -27,7 +27,7 @@
 qed;
 
 lemma K': "A --> B --> A";
-proof single+; txt {* better use sufficient-to-show here \dots *};
+proof single+   -- {* better use sufficient-to-show here \dots *};
   assume A;
   show A; .;
 qed;