# HG changeset patch
# User wenzelm
# Date 936361347 -7200
# Node ID ebd975549ffe9fdb49d60cd1751541654b322214
# Parent  3ee96dccdd3901895cdd1cc208ed4204ad9666ec
tuned K;

diff -r 3ee96dccdd39 -r ebd975549ffe src/HOL/Isar_examples/BasicLogic.thy
--- a/src/HOL/Isar_examples/BasicLogic.thy	Fri Sep 03 14:22:12 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Fri Sep 03 14:22:27 1999 +0200
@@ -17,6 +17,7 @@
   show A; .;
 qed;
 
+
 lemma K: "A --> B --> A";
 proof;
   assume A;
@@ -27,11 +28,21 @@
 qed;
 
 lemma K': "A --> B --> A";
+proof;
+  assume A;
+  thus "B --> A"; ..;
+qed;
+
+lemma K'': "A --> B --> A";
 proof intro;
   assume A;
   show A; .;
 qed;
 
+lemma K''': "A --> B --> A";
+  by intro;
+
+
 lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
 proof;
   assume "A --> B --> C";