changeset 7005 | cc778d613217 |
parent 7001 | 8121e11ed765 |
child 7133 | 64c9f2364dae |
--- 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;