changeset 7233 | 75cc3a327bd4 |
parent 7133 | 64c9f2364dae |
child 7306 | cd0533d52e55 |
--- 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;