diff -r 4939494ed791 -r ce654b0e6d69 src/Doc/Tutorial/Misc/Plus.thy
--- a/src/Doc/Tutorial/Misc/Plus.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/Doc/Tutorial/Misc/Plus.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -10,7 +10,7 @@
 
 text\<open>\noindent and prove\<close>
 (*<*)
-lemma [simp]: "!m. add m n = m+n"
+lemma [simp]: "\<forall>m. add m n = m+n"
 apply(induct_tac n)
 by(auto)
 (*>*)