src/HOLCF/Product_Cpo.thy
changeset 29533 7f4a32134447
parent 29531 2eb29775b0b6
child 29535 08824fad8879
     1.1 --- a/src/HOLCF/Product_Cpo.thy	Wed Jan 14 18:05:05 2009 -0800
     1.2 +++ b/src/HOLCF/Product_Cpo.thy	Wed Jan 14 18:18:48 2009 -0800
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* The cpo of cartesian products *}
     1.5  
     1.6  theory Product_Cpo
     1.7 -imports Ffun
     1.8 +imports Cont
     1.9  begin
    1.10  
    1.11  defaultsort cpo
    1.12 @@ -192,12 +192,13 @@
    1.13    assumes f: "cont (\<lambda>x. f x)"
    1.14    assumes g: "cont (\<lambda>x. g x)"
    1.15    shows "cont (\<lambda>x. (f x, g x))"
    1.16 -apply (rule cont2cont_app2 [OF cont2cont_lambda cont_pair2 g])
    1.17 -apply (rule cont2cont_app2 [OF cont_const cont_pair1 f])
    1.18 +apply (rule cont2cont_apply [OF _ cont_pair1 f])
    1.19 +apply (rule cont2cont_apply [OF _ cont_pair2 g])
    1.20 +apply (rule cont_const)
    1.21  done
    1.22  
    1.23 -lemmas cont2cont_fst [cont2cont] = cont2cont_app3 [OF cont_fst]
    1.24 +lemmas cont2cont_fst [cont2cont] = cont2cont_compose [OF cont_fst]
    1.25  
    1.26 -lemmas cont2cont_snd [cont2cont] = cont2cont_app3 [OF cont_snd]
    1.27 +lemmas cont2cont_snd [cont2cont] = cont2cont_compose [OF cont_snd]
    1.28  
    1.29  end