src/HOLCF/Cprod.thy
changeset 27413 3154f3765cc7
parent 27310 d0229bc6c461
child 29138 661a8db7e647
     1.1 --- a/src/HOLCF/Cprod.thy	Tue Jul 01 01:28:44 2008 +0200
     1.2 +++ b/src/HOLCF/Cprod.thy	Tue Jul 01 02:19:53 2008 +0200
     1.3 @@ -129,7 +129,7 @@
     1.4  
     1.5  lemma thelub_cprod:
     1.6    "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
     1.7 -    \<Longrightarrow> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
     1.8 +    \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
     1.9  by (rule lub_cprod [THEN thelubI])
    1.10  
    1.11  instance "*" :: (cpo, cpo) cpo
    1.12 @@ -326,7 +326,7 @@
    1.13  done
    1.14  
    1.15  lemma thelub_cprod2:
    1.16 -  "chain S \<Longrightarrow> lub (range S) = <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
    1.17 +  "chain S \<Longrightarrow> (\<Squnion>i. S i) = <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
    1.18  by (rule lub_cprod2 [THEN thelubI])
    1.19  
    1.20  lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"