--- a/src/FOL/IFOL.thy Fri Sep 16 18:09:13 2016 +0200
+++ b/src/FOL/IFOL.thy Fri Sep 16 21:28:09 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)"