tuned;
authorwenzelm
Fri Apr 23 17:01:50 1999 +0200 (1999-04-23)
changeset 6504b275757bfdcb
parent 6503 914729515c26
child 6505 2863855a6902
tuned;
src/HOL/Isar_examples/BasicLogic.thy
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Fri Apr 23 17:01:36 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Fri Apr 23 17:01:50 1999 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4    qed;
     1.5  qed;
     1.6  
     1.7 -lemma K: "A --> B --> A";
     1.8 +lemma K': "A --> B --> A";
     1.9  proof single*;
    1.10    assume A;
    1.11    show A; .;
    1.12 @@ -122,7 +122,7 @@
    1.13  qed;
    1.14  
    1.15  lemma "(EX x. P(f(x))) --> (EX x. P(x))";
    1.16 -by blast;
    1.17 +  by blast;
    1.18  
    1.19  
    1.20  end;