--- 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?*}