author | wenzelm |
Wed, 05 Dec 2001 03:19:47 +0100 | |
changeset 12387 | fe2353a8d1e8 |
parent 12386 | 9c38ec9eca1c |
child 12388 | c845fec1ac94 |
--- a/src/HOL/Isar_examples/BasicLogic.thy Wed Dec 05 03:19:14 2001 +0100 +++ b/src/HOL/Isar_examples/BasicLogic.thy Wed Dec 05 03:19:47 2001 +0100 @@ -113,7 +113,7 @@ *} lemma "A --> B --> A" -proof intro +proof (intro impI) assume A show A . qed @@ -123,7 +123,7 @@ *} lemma "A --> B --> A" - by intro + by (intro impI) text {* Just like $\idt{rule}$, the $\idt{intro}$ and $\idt{elim}$ proof