src/HOLCF/Cprod.thy
changeset 40002 c5b5f7a3a3b1
parent 39987 8c2f449af35a
child 40502 8e92772bc0e8
     1.1 --- a/src/HOLCF/Cprod.thy	Mon Oct 11 16:24:44 2010 -0700
     1.2 +++ b/src/HOLCF/Cprod.thy	Mon Oct 11 21:35:31 2010 -0700
     1.3 @@ -51,7 +51,7 @@
     1.4  unfolding cprod_map_def by simp
     1.5  
     1.6  lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
     1.7 -unfolding expand_cfun_eq by auto
     1.8 +unfolding cfun_eq_iff by auto
     1.9  
    1.10  lemma cprod_map_map:
    1.11    "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =