src/HOL/Isar_examples/BasicLogic.thy
changeset 12387 fe2353a8d1e8
parent 10636 d1efa59ea259
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Wed Dec 05 03:19:14 2001 +0100
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Wed Dec 05 03:19:47 2001 +0100
     1.3 @@ -113,7 +113,7 @@
     1.4  *}
     1.5  
     1.6  lemma "A --> B --> A"
     1.7 -proof intro
     1.8 +proof (intro impI)
     1.9    assume A
    1.10    show A .
    1.11  qed
    1.12 @@ -123,7 +123,7 @@
    1.13  *}
    1.14  
    1.15  lemma "A --> B --> A"
    1.16 -  by intro
    1.17 +  by (intro impI)
    1.18  
    1.19  text {*
    1.20   Just like $\idt{rule}$, the $\idt{intro}$ and $\idt{elim}$ proof