src/HOL/Isar_examples/BasicLogic.thy

     show A; .;
   qed;
 qed;
 
 lemma K': "A --> B --> A";
-proof intro+;
+proof intro;
   assume A;
   show A; .;
 qed;
 
 lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";