diff -r eef4e9081bea -r 07ec57376051 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -968,14 +968,14 @@
 apply fast
 apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
 apply (simp, rule conjI, (rule HOL.refl)+)
-apply simp
+apply simp apply (rule conjI, simp) apply (simp add: nat_add_distrib)
 apply (rule progression_refl)
 
  (* case b= False *)
 apply simp
 apply (rule_tac ?instrs1.0 = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
 apply (simp, rule conjI, (rule HOL.refl)+)
-apply simp
+apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
 apply fast
 
 (* case exit Loop *)
@@ -1003,7 +1003,7 @@
 apply fast
 apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
 apply (simp, rule conjI, rule HOL.refl, rule HOL.refl)
-apply simp
+apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
 apply (rule progression_refl)