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/HOLCF/Library/Sum_Cpo.thy
changeset 41323 ae1c227534f5
parent 41321 4e72b6fc9dd4
child 41392 d1ff42a70f77 
--- a/src/HOL/HOLCF/Library/Sum_Cpo.thy	Mon Dec 20 09:41:55 2010 -0800
+++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy	Mon Dec 20 09:48:16 2010 -0800
@@ -338,7 +338,7 @@
   where "sum_map' f g \<equiv> Abs_cfun (sum_map (Rep_cfun f) (Rep_cfun g))"
 
 lemma sum_map_ID [domain_map_ID]: "sum_map' ID ID = ID"
-by (simp add: ID_def cfun_eq_iff Abs_cfun_inverse2 sum_map.identity)
+by (simp add: ID_def cfun_eq_iff sum_map.identity)
 
 lemma deflation_sum_map [domain_deflation]:
   "\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (sum_map' d1 d2)"
isabelle