| changeset 15481 | fc075ae929e4 |
| parent 15236 | f289e8ba2bb3 |
| child 15860 | a344c4284972 |
--- a/src/HOL/MicroJava/Comp/CorrComp.thy Sun Jan 30 20:48:50 2005 +0100 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy Tue Feb 01 18:01:57 2005 +0100 @@ -295,7 +295,7 @@ apply simp apply assumption apply simp apply assumption apply simp -apply (subst method_rec) apply simp +apply (simplesubst method_rec) apply simp apply force apply simp apply (simp only: map_add_def)