# HG changeset patch
# User hoelzl
# Date 1265291108 -3600
# Node ID 5312d2ffee3bef8bfa1b515a9cee6eaf3f5f4099
# Parent  5e492a862b344e01b46c669113eab37fa04eadd4
Changed 'bounded unique existential quantifiers' from a constant to syntax translation.

diff -r 5e492a862b34 -r 5312d2ffee3b src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Feb 04 13:36:52 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Feb 04 14:45:08 2010 +0100
@@ -5906,7 +5906,7 @@
       using c and zero_le_dist[of x y] by auto
     hence "y = x" by auto
   }
-  ultimately show ?thesis unfolding Bex1_def using `x\<in>s` by blast+
+  ultimately show ?thesis using `x\<in>s` by blast+
 qed
 
 subsection{* Edelstein fixed point theorem.                                            *}
@@ -5923,7 +5923,7 @@
     hence "x = y" using `x\<in>s` and dist[THEN bspec[where x=x], THEN bspec[where x=y]]
       unfolding g[THEN bspec[where x=x], OF `x\<in>s`]
       unfolding g[THEN bspec[where x=y], OF `y\<in>s`] by auto  }
-  thus ?thesis unfolding Bex1_def using `x\<in>s` and g by blast+
+  thus ?thesis using `x\<in>s` and g by blast+
 next
   case True
   then obtain x where [simp]:"x\<in>s" and "g x \<noteq> x" by auto
@@ -6028,7 +6028,7 @@
   { fix x assume "x\<in>s" "g x = x" "x\<noteq>a"
     hence "False" using dist[THEN bspec[where x=a], THEN bspec[where x=x]]
       using `g a = a` and `a\<in>s` by auto  }
-  ultimately show "\<exists>!x\<in>s. g x = x" unfolding Bex1_def using `a\<in>s` by blast
+  ultimately show "\<exists>!x\<in>s. g x = x" using `a\<in>s` by blast
 qed
 
 end
diff -r 5e492a862b34 -r 5312d2ffee3b src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Feb 04 13:36:52 2010 +0100
+++ b/src/HOL/Set.thy	Thu Feb 04 14:45:08 2010 +0100
@@ -161,14 +161,12 @@
 consts
   Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
   Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
-  Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
 
 local
 
 defs
   Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
   Bex_def:      "Bex A P        == EX x. x:A & P(x)"
-  Bex1_def:     "Bex1 A P       == EX! x. x:A & P(x)"
 
 syntax
   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
@@ -195,7 +193,7 @@
 translations
   "ALL x:A. P"  == "Ball A (%x. P)"
   "EX x:A. P"   == "Bex A (%x. P)"
-  "EX! x:A. P"  == "Bex1 A (%x. P)"
+  "EX! x:A. P"  => "EX! x. x:A & P"
   "LEAST x:A. P" => "LEAST x. x:A & P"
 
 syntax (output)