diff -r 23bd419144eb -r 2fa13b499975 doc-src/TutorialI/Rules/Forward.thy
--- a/doc-src/TutorialI/Rules/Forward.thy	Wed Dec 05 14:32:10 2001 +0100
+++ b/doc-src/TutorialI/Rules/Forward.thy	Wed Dec 05 15:36:36 2001 +0100
@@ -117,7 +117,7 @@
 *}
 
 lemma "2 \<le> u \<Longrightarrow> u*m \<noteq> Suc(u*n)"
-apply intro
+apply (intro notI)
 txt{*
 before using arg_cong
 @{subgoals[display,indent=0,margin=65]}