Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/Comp/LemmasComp.thy
changeset 69661 a03a63b81f44
parent 67613 ce654b0e6d69 
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -167,12 +167,8 @@
 
 
 lemma comp_wf_syscls: "wf_syscls (comp G) = wf_syscls G"
-  apply (simp add: wf_syscls_def comp_def compClass_def split_beta)
-  apply (simp add: image_comp)
-  apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls).
-                      (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
-   apply simp
-  apply (simp add: fun_eq_iff split_beta)
+  apply (simp add: wf_syscls_def comp_def compClass_def split_beta cong: image_cong_simp)
+  apply (simp add: image_comp cong: image_cong_simp)
   done
isabelle