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/ZF/Zet.thy
changeset 69661 a03a63b81f44
parent 67613 ce654b0e6d69 
--- a/src/HOL/ZF/Zet.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/ZF/Zet.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -37,7 +37,7 @@
   apply (rule_tac x="Repl z (g o (inv_into A f))" in exI)
   apply (simp add: explode_Repl_eq)
   apply (subgoal_tac "explode z = f ` A")
-  apply (simp_all add: image_comp [symmetric])
+  apply (simp_all add: image_image cong: image_cong_simp)
   done
 
 lemma zet_image_mem:
@@ -98,7 +98,7 @@
 lemma zimplode_zexplode: "zimplode (zexplode z) = z"
   apply (simp add: zimplode_def zexplode_def)
   apply (subst Abs_zet_inverse)
-  apply (auto simp add: explode_mem_zet implode_explode)
+  apply (auto simp add: explode_mem_zet)
   done  
 
 lemma zin_zexplode_eq: "zin x (zexplode A) = Elem x A"
isabelle