intro+;
authorwenzelm
Tue Aug 17 17:34:43 1999 +0200 (1999-08-17)
changeset 723375cc3a327bd4
parent 7232 6e7b6b8490e0
child 7234 1ba436add81b
intro+;
src/HOL/Isar_examples/BasicLogic.thy
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Tue Aug 17 17:34:18 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Tue Aug 17 17:34:43 1999 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  qed;
     1.5  
     1.6  lemma K': "A --> B --> A";
     1.7 -proof single+   -- {* better use sufficient-to-show here \dots *};
     1.8 +proof intro+;
     1.9    assume A;
    1.10    show A; .;
    1.11  qed;