--- a/src/Doc/Tutorial/Sets/Examples.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/Doc/Tutorial/Sets/Examples.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -155,7 +155,7 @@
 by blast
 
 definition prime :: "nat set" where
-    "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
+    "prime == {p. 1<p & (\<forall>m. m dvd p \<longrightarrow> m=1 \<or> m=p)}"
 
 lemma "{p*q | p q. p\<in>prime \<and> q\<in>prime} =
        {z. \<exists>p q. z = p*q \<and> p\<in>prime \<and> q\<in>prime}"