changeset 41323 | ae1c227534f5 |
parent 41321 | 4e72b6fc9dd4 |
child 41437 | 5bc117c382ec |
--- 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 \<equiv> 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 \<Longrightarrow> deflation (list_map d)"