src/FOL/IFOL.thy
changeset 63901 4ce989e962e0
parent 62020 5d208fd2507d
child 63906 fa799a8e4adc
     1.1 --- a/src/FOL/IFOL.thy	Fri Sep 16 18:09:13 2016 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Fri Sep 16 21:28:09 2016 +0200
     1.3 @@ -275,10 +275,10 @@
     1.4  text \<open>
     1.5    NOTE THAT the following 2 quantifications:
     1.6  
     1.7 -    \<^item> EX!x such that [EX!y such that P(x,y)]     (sequential)
     1.8 -    \<^item> EX!x,y such that P(x,y)                    (simultaneous)
     1.9 +    \<^item> \<exists>!x such that [\<exists>!y such that P(x,y)]     (sequential)
    1.10 +    \<^item> \<exists>!x,y such that P(x,y)                   (simultaneous)
    1.11  
    1.12 -  do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential.
    1.13 +  do NOT mean the same thing. The parser treats \<exists>!x y.P(x,y) as sequential.
    1.14  \<close>
    1.15  
    1.16  lemma ex1I: "P(a) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> x = a) \<Longrightarrow> \<exists>!x. P(x)"