src/HOLCF/Cprod.thy
changeset 16093 cdcbf5a7f38d
parent 16081 81a4b4a245b0
child 16210 5d1b752cacc1
     1.1 --- a/src/HOLCF/Cprod.thy	Fri May 27 00:15:24 2005 +0200
     1.2 +++ b/src/HOLCF/Cprod.thy	Fri May 27 00:16:18 2005 +0200
     1.3 @@ -138,14 +138,14 @@
     1.4  apply (rule contlubI [rule_format])
     1.5  apply (subst thelub_cprod)
     1.6  apply (erule monofun_pair1 [THEN ch2ch_monofun])
     1.7 -apply (simp add: lub_const [THEN thelubI])
     1.8 +apply (simp add: thelub_const)
     1.9  done
    1.10  
    1.11  lemma contlub_pair2: "contlub (\<lambda>y. (x, y))"
    1.12  apply (rule contlubI [rule_format])
    1.13  apply (subst thelub_cprod)
    1.14  apply (erule monofun_pair2 [THEN ch2ch_monofun])
    1.15 -apply (simp add: lub_const [THEN thelubI])
    1.16 +apply (simp add: thelub_const)
    1.17  done
    1.18  
    1.19  lemma cont_pair1: "cont (\<lambda>x. (x, y))"