tuned;
authorwenzelm
Fri Dec 08 15:10:36 2000 +0100 (2000-12-08)
changeset 10636d1efa59ea259
parent 10635 b115460e5c50
child 10637 41d309b48afe
tuned;
src/HOL/Isar_examples/BasicLogic.thy
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Fri Dec 08 00:04:34 2000 +0100
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Fri Dec 08 15:10:36 2000 +0100
     1.3 @@ -368,10 +368,10 @@
     1.4   binds term abbreviations by higher-order pattern matching.
     1.5  *}
     1.6  
     1.7 -lemma "(EX x. P (f x)) --> (EX x. P x)"
     1.8 +lemma "(EX x. P (f x)) --> (EX y. P y)"
     1.9  proof
    1.10    assume "EX x. P (f x)"
    1.11 -  thus "EX x. P x"
    1.12 +  thus "EX y. P y"
    1.13    proof (rule exE)             -- {*
    1.14      rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
    1.15    *}
    1.16 @@ -390,10 +390,10 @@
    1.17   the text as follows.
    1.18  *}
    1.19  
    1.20 -lemma "(EX x. P (f x)) --> (EX x. P x)"
    1.21 +lemma "(EX x. P (f x)) --> (EX y. P y)"
    1.22  proof
    1.23    assume "EX x. P (f x)"
    1.24 -  thus "EX x. P x"
    1.25 +  thus "EX y. P y"
    1.26    proof
    1.27      fix a
    1.28      assume "P (f a)"
    1.29 @@ -408,11 +408,11 @@
    1.30   generalized existence reasoning.
    1.31  *}
    1.32  
    1.33 -lemma "(EX x. P (f x)) --> (EX x. P x)"
    1.34 +lemma "(EX x. P (f x)) --> (EX y. P y)"
    1.35  proof
    1.36    assume "EX x. P (f x)"
    1.37 -  then obtain a where "P (f a)" by blast
    1.38 -  thus "EX x. P x" ..
    1.39 +  then obtain a where "P (f a)" ..
    1.40 +  thus "EX y. P y" ..
    1.41  qed
    1.42  
    1.43  text {*