equal
deleted
inserted
replaced
347 apply (subgoal_tac "\<forall>x\<in>set ms. fst ((Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca)) x) = fst x") |
347 apply (subgoal_tac "\<forall>x\<in>set ms. fst ((Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca)) x) = fst x") |
348 prefer 2 apply (simp (no_asm_simp) add: compMethod_def split_beta) |
348 prefer 2 apply (simp (no_asm_simp) add: compMethod_def split_beta) |
349 apply (simp add: map_of_map2) |
349 apply (simp add: map_of_map2) |
350 apply (simp (no_asm_simp) add: compMethod_def split_beta) |
350 apply (simp (no_asm_simp) add: compMethod_def split_beta) |
351 |
351 |
352 -- "remaining subgoals" |
352 \<comment> "remaining subgoals" |
353 apply (auto intro: inv_f_eq simp add: inj_on_def is_class_def) |
353 apply (auto intro: inv_f_eq simp add: inj_on_def is_class_def) |
354 done |
354 done |
355 |
355 |
356 |
356 |
357 |
357 |