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