diff -r f5401162c9f0 -r ecdfd237ffee doc-src/TutorialI/Rules/Tacticals.thy
--- a/doc-src/TutorialI/Rules/Tacticals.thy	Mon Oct 08 14:19:42 2001 +0200
+++ b/doc-src/TutorialI/Rules/Tacticals.thy	Mon Oct 08 14:29:02 2001 +0200
@@ -12,7 +12,7 @@
 by (drule mp, assumption)+
 
 text{*ORELSE with REPEAT*}
-lemma "\<lbrakk>Q\<longrightarrow>R; P\<longrightarrow>Q; x<#5\<longrightarrow>P;  Suc x < #5\<rbrakk> \<Longrightarrow> R" 
+lemma "\<lbrakk>Q\<longrightarrow>R; P\<longrightarrow>Q; x<5\<longrightarrow>P;  Suc x < 5\<rbrakk> \<Longrightarrow> R" 
 by (drule mp, (assumption|arith))+
 
 text{*exercise: what's going on here?*}