--- a/src/HOL/Isar_examples/BasicLogic.thy Fri Dec 08 00:04:34 2000 +0100
+++ b/src/HOL/Isar_examples/BasicLogic.thy Fri Dec 08 15:10:36 2000 +0100
@@ -368,10 +368,10 @@
binds term abbreviations by higher-order pattern matching.
*}
-lemma "(EX x. P (f x)) --> (EX x. P x)"
+lemma "(EX x. P (f x)) --> (EX y. P y)"
proof
assume "EX x. P (f x)"
- thus "EX x. P x"
+ thus "EX y. P y"
proof (rule exE) -- {*
rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
*}
@@ -390,10 +390,10 @@
the text as follows.
*}
-lemma "(EX x. P (f x)) --> (EX x. P x)"
+lemma "(EX x. P (f x)) --> (EX y. P y)"
proof
assume "EX x. P (f x)"
- thus "EX x. P x"
+ thus "EX y. P y"
proof
fix a
assume "P (f a)"
@@ -408,11 +408,11 @@
generalized existence reasoning.
*}
-lemma "(EX x. P (f x)) --> (EX x. P x)"
+lemma "(EX x. P (f x)) --> (EX y. P y)"
proof
assume "EX x. P (f x)"
- then obtain a where "P (f a)" by blast
- thus "EX x. P x" ..
+ then obtain a where "P (f a)" ..
+ thus "EX y. P y" ..
qed
text {*