author wenzelm Fri Dec 08 15:10:36 2000 +0100 (2000-12-08) changeset 10636 d1efa59ea259 parent 10635 b115460e5c50 child 10637 41d309b48afe
tuned;
```     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 {*
```