--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Mon Jun 11 11:06:00 2007 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Mon Jun 11 11:06:04 2007 +0200
@@ -522,7 +522,8 @@
lemma pc_succs_shift: "pc'\<in>set (succs i (pc'' + n))
\<Longrightarrow> ((pc' - n) \<in>set (succs i pc''))"
apply (induct i)
-apply (arith|simp)+
+apply simp_all
+apply arith
done
@@ -530,7 +531,8 @@
\<forall> b. ((i = (Goto b) \<or> i=(Ifcmpeq b)) \<longrightarrow> 0 \<le> (int pc'' + b)) \<rbrakk>
\<Longrightarrow> n \<le> pc'"
apply (induct i)
-apply (arith|simp)+
+apply simp_all
+apply arith
done