src/HOL/HOLCF/Product_Cpo.thy
changeset 61424 c3658c18b7bc
parent 58880 0baae4311a9f
child 62175 8ffc4d0e652d
     1.1 --- a/src/HOL/HOLCF/Product_Cpo.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/HOLCF/Product_Cpo.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -169,7 +169,7 @@
     1.4  lemma Pair_strict [simp]: "(\<bottom>, \<bottom>) = \<bottom>"
     1.5  by simp
     1.6  
     1.7 -lemma split_strict [simp]: "split f \<bottom> = f \<bottom> \<bottom>"
     1.8 +lemma split_strict [simp]: "case_prod f \<bottom> = f \<bottom> \<bottom>"
     1.9  unfolding split_def by simp
    1.10  
    1.11  subsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *}
    1.12 @@ -235,7 +235,7 @@
    1.13    have "cont (\<lambda>(x, y). f (x, y))"
    1.14      by (intro cont2cont_case_prod f1 f2 cont2cont)
    1.15    thus "cont f"
    1.16 -    by (simp only: split_eta)
    1.17 +    by (simp only: case_prod_eta)
    1.18  qed
    1.19  
    1.20  lemma prod_cont_iff: