diff -r 4939494ed791 -r ce654b0e6d69 src/Doc/Sugar/Sugar.thy
--- a/src/Doc/Sugar/Sugar.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/Doc/Sugar/Sugar.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -55,7 +55,7 @@
 
 \subsection{Logic}
 
-The formula @{prop[source]"\<not>(\<exists>x. P x)"} is typeset as @{prop"~(EX x. P x)"}.
+The formula @{prop[source]"\<not>(\<exists>x. P x)"} is typeset as @{prop"\<not>(\<exists>x. P x)"}.
 
 The predefined constructs @{text"if"}, @{text"let"} and
 @{text"case"} are set in sans serif font to distinguish them from