src/HOLCF/Sprod.thy
changeset 40002 c5b5f7a3a3b1
parent 39987 8c2f449af35a
child 40046 ba2e41c8b725
     1.1 --- a/src/HOLCF/Sprod.thy	Mon Oct 11 16:24:44 2010 -0700
     1.2 +++ b/src/HOLCF/Sprod.thy	Mon Oct 11 21:35:31 2010 -0700
     1.3 @@ -250,7 +250,7 @@
     1.4  by (cases "x = \<bottom> \<or> y = \<bottom>") auto
     1.5  
     1.6  lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID"
     1.7 -unfolding sprod_map_def by (simp add: expand_cfun_eq eta_cfun)
     1.8 +unfolding sprod_map_def by (simp add: cfun_eq_iff eta_cfun)
     1.9  
    1.10  lemma sprod_map_map:
    1.11    "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>