330 (\<lambda>(sig,rT,maxl,b). Eps (wt_method G C (snd sig) rT maxl b)) |
330 (\<lambda>(sig,rT,maxl,b). Eps (wt_method G C (snd sig) rT maxl b)) |
331 (\<epsilon>(sg,rT,maxl,b). (sg, rT, maxl, b) \<in> set mdecls \<and> sg = sig)) |
331 (\<epsilon>(sg,rT,maxl,b). (sg, rT, maxl, b) \<in> set mdecls \<and> sg = sig)) |
332 (\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m" |
332 (\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m" |
333 by - (drule bspec, assumption, |
333 by - (drule bspec, assumption, |
334 clarsimp dest!: wtl_method_correct, |
334 clarsimp dest!: wtl_method_correct, |
335 clarsimp intro!: selectI simp add: unique_epsilon) |
335 clarsimp intro!: someI simp add: unique_epsilon) |
336 qed |
336 qed |
337 qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def) |
337 qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def) |
338 qed |
338 qed |
339 qed |
339 qed |
340 |
340 |