tuned;

--- a/src/HOL/Isar_examples/BasicLogic.thy	Fri Apr 23 17:01:36 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Fri Apr 23 17:01:50 1999 +0200
@@ -23,7 +23,7 @@
   qed;
 qed;
 
-lemma K: "A --> B --> A";
+lemma K': "A --> B --> A";
 proof single*;
   assume A;
   show A; .;
@@ -122,7 +122,7 @@
 qed;
 
 lemma "(EX x. P(f(x))) --> (EX x. P(x))";
-by blast;
+  by blast;
 
 
 end;