# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1474105273 -7200
# Node ID fa799a8e4adcecadd76bda615eae7e280ed2102e
# Parent  1c3dcb5fe6cbce1ef8feea7b4066974a0e933e1e
repair LaTeX dropout from f83ef97d8d7d

diff -r 1c3dcb5fe6cb -r fa799a8e4adc src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Fri Sep 16 12:30:55 2016 +0200
+++ b/src/FOL/IFOL.thy	Sat Sep 17 11:41:13 2016 +0200
@@ -275,10 +275,10 @@
 text \<open>
   NOTE THAT the following 2 quantifications:
 
-    \<^item> \<exists>!x such that [\<exists>!y such that P(x,y)]     (sequential)
-    \<^item> \<exists>!x,y such that P(x,y)                   (simultaneous)
+    \<^item> \<open>\<exists>!x\<close> such that [\<open>\<exists>!y\<close> such that P(x,y)]   (sequential)
+    \<^item> \<open>\<exists>!x,y\<close> such that P(x,y)                   (simultaneous)
 
-  do NOT mean the same thing. The parser treats \<exists>!x y.P(x,y) as sequential.
+  do NOT mean the same thing. The parser treats \<open>\<exists>!x y.P(x,y)\<close> as sequential.
 \<close>
 
 lemma ex1I: "P(a) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> x = a) \<Longrightarrow> \<exists>!x. P(x)"