--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Feb 05 11:14:34 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Feb 05 11:15:16 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
--- a/src/HOL/Set.thy Fri Feb 05 11:14:34 2010 +0100
+++ b/src/HOL/Set.thy Fri Feb 05 11:15:16 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)