| changeset 14025 | d9b155757dc8 |
| parent 13837 | 8dd150d36c65 |
| child 14045 | a34d89ce6097 |
--- a/src/HOL/MicroJava/Comp/CorrComp.thy Tue May 13 08:59:21 2003 +0200 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy Wed May 14 10:22:09 2003 +0200 @@ -300,7 +300,7 @@ apply (subst method_rec) apply simp apply force apply assumption -apply (simp only: override_def) +apply (simp only: map_add_def) apply (split option.split) apply (rule conjI) apply force