| changeset 33640 | 0d82107dc07a |
| parent 32960 | 69916a850301 |
| child 33954 | 1bc3b688548c |
--- a/src/HOL/MicroJava/J/WellForm.thy Thu Nov 12 17:21:48 2009 +0100 +++ b/src/HOL/MicroJava/J/WellForm.thy Thu Nov 12 17:21:51 2009 +0100 @@ -284,8 +284,7 @@ apply (frule fields_rec, assumption) apply (rule HOL.trans) apply (simp add: o_def) -apply (simp (no_asm_use) - add: split_beta split_def o_def map_compose [THEN sym] del: map_compose) +apply (simp (no_asm_use) add: split_beta split_def o_def) done lemma method_Object [simp]: