# HG changeset patch
# User wenzelm
# Date 924879710 -7200
# Node ID b275757bfdcbbda89e88744abbd027935f8da44b
# Parent  914729515c265781fb6fb96efae39d22c7ca4470
tuned;

diff -r 914729515c26 -r b275757bfdcb src/HOL/Isar_examples/BasicLogic.thy
--- 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;