src/FOL/IFOL.thy
changeset 63906 fa799a8e4adc
parent 63901 4ce989e962e0
child 68816 5a53724fe247
     1.1 --- a/src/FOL/IFOL.thy	Fri Sep 16 12:30:55 2016 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Sat Sep 17 11:41:13 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> \<exists>!x such that [\<exists>!y such that P(x,y)]     (sequential)
     1.8 -    \<^item> \<exists>!x,y such that P(x,y)                   (simultaneous)
     1.9 +    \<^item> \<open>\<exists>!x\<close> such that [\<open>\<exists>!y\<close> such that P(x,y)]   (sequential)
    1.10 +    \<^item> \<open>\<exists>!x,y\<close> such that P(x,y)                   (simultaneous)
    1.11  
    1.12 -  do NOT mean the same thing. The parser treats \<exists>!x y.P(x,y) as sequential.
    1.13 +  do NOT mean the same thing. The parser treats \<open>\<exists>!x y.P(x,y)\<close> 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)"