# HG changeset patch # User huffman # Date 1292867296 28800 # Node ID ae1c227534f540f463762b62aee9571ec260e6dd # Parent 43a5b9a0ee8a82cd390e02aaf860451b88e6d7c3 simplify proofs diff -r 43a5b9a0ee8a -r ae1c227534f5 src/HOL/HOLCF/Library/List_Predomain.thy --- a/src/HOL/HOLCF/Library/List_Predomain.thy Mon Dec 20 09:41:55 2010 -0800 +++ b/src/HOL/HOLCF/Library/List_Predomain.thy Mon Dec 20 09:48:16 2010 -0800 @@ -139,7 +139,7 @@ where "list_map f \ Abs_cfun (map (Rep_cfun f))" lemma list_map_ID [domain_map_ID]: "list_map ID = ID" -by (simp add: ID_def cfun_eq_iff Abs_cfun_inverse2) +by (simp add: ID_def) lemma deflation_list_map [domain_deflation]: "deflation d \ deflation (list_map d)" diff -r 43a5b9a0ee8a -r ae1c227534f5 src/HOL/HOLCF/Library/Sum_Cpo.thy --- 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 \ 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]: "\deflation d1; deflation d2\ \ deflation (sum_map' d1 d2)"