diff -r f5401162c9f0 -r ecdfd237ffee doc-src/TutorialI/Misc/natsum.thy
--- a/doc-src/TutorialI/Misc/natsum.thy	Mon Oct 08 14:19:42 2001 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy	Mon Oct 08 14:29:02 2001 +0200
@@ -66,7 +66,7 @@
 simple arithmetic goals automatically:
 *}
 
-lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
+lemma "\<lbrakk> \<not> m < n; m < n + (1::nat) \<rbrakk> \<Longrightarrow> m = n"
 (*<*)by(auto)(*>*)
 
 text{*\noindent
@@ -75,7 +75,7 @@
 In consequence, @{text auto} cannot prove this slightly more complex goal:
 *}
 
-lemma "\<not> m < n \<and> m < n+1 \<Longrightarrow> m = n";
+lemma "\<not> m < n \<and> m < n + (1::nat) \<Longrightarrow> m = n";
 (*<*)by(arith)(*>*)
 
 text{*\noindent