# HG changeset patch
# User wenzelm
# Date 976284636 -3600
# Node ID d1efa59ea259a7111eb39f7f54c102c4d2dbf2c1
# Parent  b115460e5c505528d35814ffe860fa33726ab7f4
tuned;

diff -r b115460e5c50 -r d1efa59ea259 src/HOL/Isar_examples/BasicLogic.thy
--- 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 {*