intro (no +);
authorwenzelm
Fri Aug 20 15:42:46 1999 +0200 (1999-08-20)
changeset 7306cd0533d52e55
parent 7305 dad3b686941c
child 7307 c065073cdb34
intro (no +);
src/HOL/Isar_examples/BasicLogic.thy
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Fri Aug 20 15:42:20 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Fri Aug 20 15:42:46 1999 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  qed;
     1.5  
     1.6  lemma K': "A --> B --> A";
     1.7 -proof intro+;
     1.8 +proof intro;
     1.9    assume A;
    1.10    show A; .;
    1.11  qed;