# HG changeset patch
# User wenzelm
# Date 1474054847 -7200
# Node ID 8c9dc05fc055592df8711ae18860b34c7392cbe9
# Parent  2359e995264107456fd892f037457f60f085c673# Parent  f83ef97d8d7d8f28260dfb1a45efd047c4018845
merged

diff -r 2359e9952641 -r 8c9dc05fc055 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Fri Sep 16 18:44:18 2016 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Fri Sep 16 21:40:47 2016 +0200
@@ -31,7 +31,9 @@
 
 \section*{HOL}
 
-The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P | Q"}, @{prop "P --> Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}.
+The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop "\<not> P"}, @{prop"P \<and> Q"},
+@{prop "P \<or> Q"}, @{prop "P \<longrightarrow> Q"}, @{prop "\<forall>x. P"}, @{prop "\<exists>x. P"}, @{prop"\<exists>! x. P"},
+@{term"THE x. P"}.
 \<^smallskip>
 
 \begin{tabular}{@ {} l @ {~::~} l @ {}}
@@ -42,10 +44,10 @@
 \subsubsection*{Syntax}
 
 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
-@{term"~(x = y)"} & @{term[source]"\<not> (x = y)"} & (\<^verbatim>\<open>~=\<close>)\\
+@{term"\<not> (x = y)"} & @{term[source]"\<not> (x = y)"} & (\<^verbatim>\<open>~=\<close>)\\
 @{term[source]"P \<longleftrightarrow> Q"} & @{term"P \<longleftrightarrow> Q"} \\
 @{term"If x y z"} & @{term[source]"If x y z"}\\
-@{term"Let e\<^sub>1 (%x. e\<^sub>2)"} & @{term[source]"Let e\<^sub>1 (\<lambda>x. e\<^sub>2)"}\\
+@{term"Let e\<^sub>1 (\<lambda>x. e\<^sub>2)"} & @{term[source]"Let e\<^sub>1 (\<lambda>x. e\<^sub>2)"}\\
 \end{supertabular}
 
 
@@ -72,10 +74,10 @@
 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
 @{term[source]"x \<ge> y"} & @{term"x \<ge> y"} & (\<^verbatim>\<open>>=\<close>)\\
 @{term[source]"x > y"} & @{term"x > y"}\\
-@{term"ALL x<=y. P"} & @{term[source]"\<forall>x. x \<le> y \<longrightarrow> P"}\\
-@{term"EX x<=y. P"} & @{term[source]"\<exists>x. x \<le> y \<and> P"}\\
+@{term "\<forall>x\<le>y. P"} & @{term[source]"\<forall>x. x \<le> y \<longrightarrow> P"}\\
+@{term "\<exists>x\<le>y. P"} & @{term[source]"\<exists>x. x \<le> y \<and> P"}\\
 \multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\
-@{term"LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\
+@{term "LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\
 \end{supertabular}
 
 
@@ -131,20 +133,20 @@
 
 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
 \<open>{a\<^sub>1,\<dots>,a\<^sub>n}\<close> & \<open>insert a\<^sub>1 (\<dots> (insert a\<^sub>n {})\<dots>)\<close>\\
-@{term"a ~: A"} & @{term[source]"\<not>(x \<in> A)"}\\
-@{term"A \<subseteq> B"} & @{term[source]"A \<le> B"}\\
-@{term"A \<subset> B"} & @{term[source]"A < B"}\\
+@{term "a \<notin> A"} & @{term[source]"\<not>(x \<in> A)"}\\
+@{term "A \<subseteq> B"} & @{term[source]"A \<le> B"}\\
+@{term "A \<subset> B"} & @{term[source]"A < B"}\\
 @{term[source]"A \<supseteq> B"} & @{term[source]"B \<le> A"}\\
 @{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\
-@{term"{x. P}"} & @{term[source]"Collect (\<lambda>x. P)"}\\
+@{term "{x. P}"} & @{term[source]"Collect (\<lambda>x. P)"}\\
 \<open>{t | x\<^sub>1 \<dots> x\<^sub>n. P}\<close> & \<open>{v. \<exists>x\<^sub>1 \<dots> x\<^sub>n. v = t \<and> P}\<close>\\
 @{term[source]"\<Union>x\<in>I. A"} & @{term[source]"UNION I (\<lambda>x. A)"} & (\texttt{UN})\\
 @{term[source]"\<Union>x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\
 @{term[source]"\<Inter>x\<in>I. A"} & @{term[source]"INTER I (\<lambda>x. A)"} & (\texttt{INT})\\
 @{term[source]"\<Inter>x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\
-@{term"ALL x:A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\
-@{term"EX x:A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\
-@{term"range f"} & @{term[source]"f ` UNIV"}\\
+@{term "\<forall>x\<in>A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\
+@{term "\<exists>x\<in>A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\
+@{term "range f"} & @{term[source]"f ` UNIV"}\\
 \end{supertabular}
 
 
@@ -225,15 +227,15 @@
 \subsubsection*{Syntax}
 
 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
-@{term"Pair a b"} & @{term[source]"Pair a b"}\\
-@{term"case_prod (\<lambda>x y. t)"} & @{term[source]"case_prod (\<lambda>x y. t)"}\\
-@{term"A \<times> B"} &  \<open>Sigma A (\<lambda>\<^raw:\_>. B)\<close>
+@{term "Pair a b"} & @{term[source]"Pair a b"}\\
+@{term "case_prod (\<lambda>x y. t)"} & @{term[source]"case_prod (\<lambda>x y. t)"}\\
+@{term "A \<times> B"} &  \<open>Sigma A (\<lambda>\<^raw:\_>. B)\<close>
 \end{tabular}
 
 Pairs may be nested. Nesting to the right is printed as a tuple,
-e.g.\ \mbox{@{term"(a,b,c)"}} is really \mbox{\<open>(a, (b, c))\<close>.}
+e.g.\ \mbox{@{term "(a,b,c)"}} is really \mbox{\<open>(a, (b, c))\<close>.}
 Pattern matching with pairs and tuples extends to all binders,
-e.g.\ \mbox{@{prop"ALL (x,y):A. P"},} @{term"{(x,y). P}"}, etc.
+e.g.\ \mbox{@{prop "\<forall>(x,y)\<in>A. P"},} @{term "{(x,y). P}"}, etc.
 
 
 \section*{Relation}
@@ -331,7 +333,7 @@
 \subsubsection*{Syntax}
 
 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{term"abs x"} & @{term[source]"abs x"}
+@{term "\<bar>x\<bar>"} & @{term[source] "abs x"}
 \end{tabular}
 
 
@@ -404,19 +406,19 @@
 
 \begin{supertabular}{@ {} l @ {~::~} l @ {}}
 @{const Finite_Set.finite} & @{term_type_only Finite_Set.finite "'a set\<Rightarrow>bool"}\\
-@{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set => nat"}\\
+@{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set \<Rightarrow> nat"}\\
 @{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\
-@{const Groups_Big.setsum} & @{term_type_only Groups_Big.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\
-@{const Groups_Big.setprod} & @{term_type_only Groups_Big.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\
+@{const Groups_Big.setsum} & @{term_type_only Groups_Big.setsum "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b::comm_monoid_add"}\\
+@{const Groups_Big.setprod} & @{term_type_only Groups_Big.setprod "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b::comm_monoid_mult"}\\
 \end{supertabular}
 
 
 \subsubsection*{Syntax}
 
 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
-@{term"setsum (%x. x) A"} & @{term[source]"setsum (\<lambda>x. x) A"} & (\<^verbatim>\<open>SUM\<close>)\\
-@{term"setsum (%x. t) A"} & @{term[source]"setsum (\<lambda>x. t) A"}\\
-@{term[source]"\<Sum>x|P. t"} & @{term"\<Sum>x|P. t"}\\
+@{term "setsum (\<lambda>x. x) A"} & @{term[source]"setsum (\<lambda>x. x) A"} & (\<^verbatim>\<open>SUM\<close>)\\
+@{term "setsum (\<lambda>x. t) A"} & @{term[source]"setsum (\<lambda>x. t) A"}\\
+@{term[source] "\<Sum>x|P. t"} & @{term"\<Sum>x|P. t"}\\
 \multicolumn{2}{@ {}l@ {}}{Similarly for \<open>\<Prod>\<close> instead of \<open>\<Sum>\<close>} & (\<^verbatim>\<open>PROD\<close>)\\
 \end{supertabular}
 
@@ -461,10 +463,10 @@
 @{term[source] "\<Union>i\<le>n. A"} & @{term[source] "\<Union>i \<in> {..n}. A"}\\
 @{term[source] "\<Union>i<n. A"} & @{term[source] "\<Union>i \<in> {..<n}. A"}\\
 \multicolumn{2}{@ {}l@ {}}{Similarly for \<open>\<Inter>\<close> instead of \<open>\<Union>\<close>}\\
-@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\
-@{term "setsum (%x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\
-@{term "setsum (%x. t) {..b}"} & @{term[source] "setsum (\<lambda>x. t) {..b}"}\\
-@{term "setsum (%x. t) {..<b}"} & @{term[source] "setsum (\<lambda>x. t) {..<b}"}\\
+@{term "setsum (\<lambda>x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\
+@{term "setsum (\<lambda>x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\
+@{term "setsum (\<lambda>x. t) {..b}"} & @{term[source] "setsum (\<lambda>x. t) {..b}"}\\
+@{term "setsum (\<lambda>x. t) {..<b}"} & @{term[source] "setsum (\<lambda>x. t) {..<b}"}\\
 \multicolumn{2}{@ {}l@ {}}{Similarly for \<open>\<Prod>\<close> instead of \<open>\<Sum>\<close>}\\
 \end{supertabular}
 
diff -r 2359e9952641 -r 8c9dc05fc055 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Fri Sep 16 18:44:18 2016 +0200
+++ b/src/FOL/IFOL.thy	Fri Sep 16 21:40:47 2016 +0200
@@ -275,10 +275,10 @@
 text \<open>
   NOTE THAT the following 2 quantifications:
 
-    \<^item> EX!x such that [EX!y such that P(x,y)]     (sequential)
-    \<^item> EX!x,y such that P(x,y)                    (simultaneous)
+    \<^item> \<exists>!x such that [\<exists>!y such that P(x,y)]     (sequential)
+    \<^item> \<exists>!x,y such that P(x,y)                   (simultaneous)
 
-  do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential.
+  do NOT mean the same thing. The parser treats \<exists>!x y.P(x,y) as sequential.
 \<close>
 
 lemma ex1I: "P(a) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> x = a) \<Longrightarrow> \<exists>!x. P(x)"
diff -r 2359e9952641 -r 8c9dc05fc055 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Fri Sep 16 18:44:18 2016 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Fri Sep 16 21:40:47 2016 +0200
@@ -1429,7 +1429,7 @@
 
 theorem UP_universal_property:
   assumes S: "s \<in> carrier S"
-  shows "EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
+  shows "\<exists>!Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
     Phi (monom P \<one> 1) = s &
     (ALL r : carrier R. Phi (monom P r 0) = h r)"
   using S eval_monom1
diff -r 2359e9952641 -r 8c9dc05fc055 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Sep 16 18:44:18 2016 +0200
+++ b/src/HOL/List.thy	Fri Sep 16 21:40:47 2016 +0200
@@ -4913,7 +4913,7 @@
 qed
 
 lemma finite_sorted_distinct_unique:
-shows "finite A \<Longrightarrow> EX! xs. set xs = A & sorted xs & distinct xs"
+shows "finite A \<Longrightarrow> \<exists>!xs. set xs = A \<and> sorted xs \<and> distinct xs"
 apply(drule finite_distinct_list)
 apply clarify
 apply(rule_tac a="sort xs" in ex1I)
diff -r 2359e9952641 -r 8c9dc05fc055 src/HOL/Matrix_LP/ComputeFloat.thy
--- a/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Sep 16 18:44:18 2016 +0200
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Sep 16 21:40:47 2016 +0200
@@ -46,7 +46,7 @@
 apply (simp add: int_of_real_sub real_int_of_real)
 done
 
-lemma real_is_int_rep: "real_is_int x \<Longrightarrow> ?! (a::int). real_of_int a = x"
+lemma real_is_int_rep: "real_is_int x \<Longrightarrow> \<exists>!(a::int). real_of_int a = x"
 by (auto simp add: real_is_int_def)
 
 lemma int_of_real_mult:
diff -r 2359e9952641 -r 8c9dc05fc055 src/HOL/Nonstandard_Analysis/NSA.thy
--- a/src/HOL/Nonstandard_Analysis/NSA.thy	Fri Sep 16 18:44:18 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSA.thy	Fri Sep 16 21:40:47 2016 +0200
@@ -1268,7 +1268,7 @@
 done
 
 text\<open>There is a unique real infinitely close\<close>
-lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> \<real> & x \<approx> t"
+lemma st_part_Ex1: "x \<in> HFinite ==> \<exists>!t::hypreal. t \<in> \<real> & x \<approx> t"
 apply (drule st_part_Ex, safe)
 apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
 apply (auto intro!: approx_unique_real)
diff -r 2359e9952641 -r 8c9dc05fc055 src/HOL/Nonstandard_Analysis/NSCA.thy
--- a/src/HOL/Nonstandard_Analysis/NSCA.thy	Fri Sep 16 18:44:18 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSCA.thy	Fri Sep 16 21:40:47 2016 +0200
@@ -350,7 +350,7 @@
 apply (simp add: Standard_HComplex st_SReal [unfolded Reals_eq_Standard])
 done
 
-lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \<in> SComplex &  x \<approx> t"
+lemma stc_part_Ex1: "x:HFinite ==> \<exists>!t. t \<in> SComplex &  x \<approx> t"
 apply (drule stc_part_Ex, safe)
 apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
 apply (auto intro!: approx_unique_complex)
diff -r 2359e9952641 -r 8c9dc05fc055 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Fri Sep 16 18:44:18 2016 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Fri Sep 16 21:40:47 2016 +0200
@@ -698,7 +698,7 @@
 lemma binary_chinese_remainder_unique_nat:
   assumes a: "coprime (m1::nat) m2"
     and nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
-  shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
+  shows "\<exists>!x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
 proof -
   from binary_chinese_remainder_nat [OF a] obtain y where
       "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
@@ -834,7 +834,7 @@
   assumes fin: "finite A"
     and nz: "\<forall>i\<in>A. m i \<noteq> 0"
     and cop: "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
-  shows "EX! x. x < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))"
+  shows "\<exists>!x. x < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))"
 proof -
   from chinese_remainder_nat [OF fin cop]
   obtain y where one: "(ALL i:A. [y = u i] (mod m i))"
diff -r 2359e9952641 -r 8c9dc05fc055 src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Fri Sep 16 18:44:18 2016 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Fri Sep 16 21:40:47 2016 +0200
@@ -270,7 +270,7 @@
   quickcheck[expect = counterexample]
 oops
 
-lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
+lemma "(\<exists>x. P x) \<longrightarrow> (\<exists>!x. P x)"
   quickcheck[random, expect = counterexample]
   quickcheck[expect = counterexample]
 oops
diff -r 2359e9952641 -r 8c9dc05fc055 src/HOL/ZF/HOLZF.thy
--- a/src/HOL/ZF/HOLZF.thy	Fri Sep 16 18:44:18 2016 +0200
+++ b/src/HOL/ZF/HOLZF.thy	Fri Sep 16 21:40:47 2016 +0200
@@ -270,7 +270,7 @@
   by (auto simp add: Fun_def Sep Domain)
 
 
-lemma unique_fun_value: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> ?! y. Elem (Opair x y) f"
+lemma unique_fun_value: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> \<exists>!y. Elem (Opair x y) f"
   by (auto simp add: Domain isFun_def)
 
 lemma fun_value_in_range: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> Elem (f\<acute>x) (Range f)"
diff -r 2359e9952641 -r 8c9dc05fc055 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Fri Sep 16 18:44:18 2016 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Fri Sep 16 21:40:47 2016 +0200
@@ -128,7 +128,7 @@
 refute [expect = genuine]
 oops
 
-lemma "EX! x. P x"
+lemma "\<exists>!x. P x"
 refute [expect = genuine]
 oops
 
@@ -152,7 +152,7 @@
 refute [expect = genuine]
 oops
 
-lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
+lemma "(\<exists>x. P x) \<longrightarrow> (\<exists>!x. P x)"
 refute [expect = genuine]
 oops
 
@@ -220,11 +220,11 @@
 refute [expect = genuine]
 oops
 
-lemma "EX! P. P"
+lemma "\<exists>!P. P"
 refute [expect = none]
 by auto
 
-lemma "EX! P. P x"
+lemma "\<exists>!P. P x"
 refute [expect = genuine]
 oops
 
@@ -280,7 +280,7 @@
 
 text \<open>Axiom of Choice: first an incorrect version ...\<close>
 
-lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
+lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
 refute [expect = genuine]
 oops
 
@@ -290,7 +290,7 @@
 refute [maxsize = 4, expect = none]
 by (simp add: choice)
 
-lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
+lemma "(\<forall>x. \<exists>!y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
 refute [maxsize = 2, expect = none]
 apply auto
   apply (simp add: ex1_implies_ex choice)
diff -r 2359e9952641 -r 8c9dc05fc055 src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Fri Sep 16 18:44:18 2016 +0200
+++ b/src/ZF/Epsilon.thy	Fri Sep 16 21:40:47 2016 +0200
@@ -305,7 +305,7 @@
 (*Not clear how to remove the P(a) condition, since the "then" part
   must refer to "a"*)
 lemma the_equality_if:
-     "P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)"
+     "P(a) ==> (THE x. P(x)) = (if (\<exists>!x. P(x)) then a else 0)"
 by (simp add: the_0 the_equality2)
 
 (*The first premise not only fixs i but ensures @{term"f\<noteq>0"}.
diff -r 2359e9952641 -r 8c9dc05fc055 src/ZF/Order.thy
--- a/src/ZF/Order.thy	Fri Sep 16 18:44:18 2016 +0200
+++ b/src/ZF/Order.thy	Fri Sep 16 21:40:47 2016 +0200
@@ -641,7 +641,7 @@
 by (unfold first_def, blast)
 
 lemma well_ord_imp_ex1_first:
-        "[| well_ord(A,r); B<=A; B\<noteq>0 |] ==> (EX! b. first(b,B,r))"
+        "[| well_ord(A,r); B<=A; B\<noteq>0 |] ==> (\<exists>!b. first(b,B,r))"
 apply (unfold well_ord_def wf_on_def wf_def first_def)
 apply (elim conjE allE disjE, blast)
 apply (erule bexE)
diff -r 2359e9952641 -r 8c9dc05fc055 src/ZF/Perm.thy
--- a/src/ZF/Perm.thy	Fri Sep 16 18:44:18 2016 +0200
+++ b/src/ZF/Perm.thy	Fri Sep 16 21:40:47 2016 +0200
@@ -137,7 +137,7 @@
 apply (blast intro!: lam_injective lam_surjective)
 done
 
-lemma RepFun_bijective: "(\<forall>y\<in>x. EX! y'. f(y') = f(y))
+lemma RepFun_bijective: "(\<forall>y\<in>x. \<exists>!y'. f(y') = f(y))
       ==> (\<lambda>z\<in>{f(y). y \<in> x}. THE y. f(y) = z) \<in> bij({f(y). y \<in> x}, x)"
 apply (rule_tac d = f in lam_bijective)
 apply (auto simp add: the_equality2)
diff -r 2359e9952641 -r 8c9dc05fc055 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Fri Sep 16 18:44:18 2016 +0200
+++ b/src/ZF/ZF.thy	Fri Sep 16 21:40:47 2016 +0200
@@ -49,7 +49,7 @@
    The resulting set (for functional P) is the same as with
    PrimReplace, but the rules are simpler. *)
 definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
-  where "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))"
+  where "Replace(A,P) == PrimReplace(A, %x y. (\<exists>!z. P(x,z)) & P(x,y))"
 
 syntax
   "_Replace"  :: "[pttrn, pttrn, i, o] => i"  ("(1{_ ./ _ \<in> _, _})")
diff -r 2359e9952641 -r 8c9dc05fc055 src/ZF/func.thy
--- a/src/ZF/func.thy	Fri Sep 16 18:44:18 2016 +0200
+++ b/src/ZF/func.thy	Fri Sep 16 21:40:47 2016 +0200
@@ -25,7 +25,7 @@
 
 (*For upward compatibility with the former definition*)
 lemma Pi_iff_old:
-    "f \<in> Pi(A,B) \<longleftrightarrow> f<=Sigma(A,B) & (\<forall>x\<in>A. EX! y. <x,y>: f)"
+    "f \<in> Pi(A,B) \<longleftrightarrow> f<=Sigma(A,B) & (\<forall>x\<in>A. \<exists>!y. <x,y>: f)"
 by (unfold Pi_def function_def, blast)
 
 lemma fun_is_function: "f \<in> Pi(A,B) ==> function(f)"
@@ -175,7 +175,7 @@
 by (simp only: lam_def cong add: RepFun_cong)
 
 lemma lam_theI:
-    "(!!x. x \<in> A ==> EX! y. Q(x,y)) ==> \<exists>f. \<forall>x\<in>A. Q(x, f`x)"
+    "(!!x. x \<in> A ==> \<exists>!y. Q(x,y)) ==> \<exists>f. \<forall>x\<in>A. Q(x, f`x)"
 apply (rule_tac x = "\<lambda>x\<in>A. THE y. Q (x,y)" in exI)
 apply simp
 apply (blast intro: theI)
diff -r 2359e9952641 -r 8c9dc05fc055 src/ZF/upair.thy
--- a/src/ZF/upair.thy	Fri Sep 16 18:44:18 2016 +0200
+++ b/src/ZF/upair.thy	Fri Sep 16 21:40:47 2016 +0200
@@ -156,11 +156,11 @@
 apply (fast dest: subst)
 done
 
-(* Only use this if you already know EX!x. P(x) *)
-lemma the_equality2: "[| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
+(* Only use this if you already know \<exists>!x. P(x) *)
+lemma the_equality2: "[| \<exists>!x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
 by blast
 
-lemma theI: "EX! x. P(x) ==> P(THE x. P(x))"
+lemma theI: "\<exists>!x. P(x) ==> P(THE x. P(x))"
 apply (erule ex1E)
 apply (subst the_equality)
 apply (blast+)
@@ -170,14 +170,14 @@
   @{term "THE x.P(x)"}  rewrites to @{term "THE x.Q(x)"} *)
 
 (*If it's "undefined", it's zero!*)
-lemma the_0: "~ (EX! x. P(x)) ==> (THE x. P(x))=0"
+lemma the_0: "~ (\<exists>!x. P(x)) ==> (THE x. P(x))=0"
 apply (unfold the_def)
 apply (blast elim!: ReplaceE)
 done
 
 (*Easier to apply than theI: conclusion has only one occurrence of P*)
 lemma theI2:
-    assumes p1: "~ Q(0) ==> EX! x. P(x)"
+    assumes p1: "~ Q(0) ==> \<exists>!x. P(x)"
         and p2: "!!x. P(x) ==> Q(x)"
     shows "Q(THE x. P(x))"
 apply (rule classical)