doc-src/TutorialI/Rules/Tacticals.thy

 
 lemma "\<lbrakk>P\<longrightarrow>Q; Q\<longrightarrow>R; R\<longrightarrow>S; P\<rbrakk> \<Longrightarrow> S"
 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?*}
 lemma "\<lbrakk>P\<and>Q\<longrightarrow>R; P\<longrightarrow>Q; P\<rbrakk> \<Longrightarrow> R"
 by (drule mp, intro?, assumption+)+