diff -r a1a481ee9425 -r cdcbf5a7f38d src/HOLCF/Cprod.thy --- a/src/HOLCF/Cprod.thy Fri May 27 00:15:24 2005 +0200 +++ b/src/HOLCF/Cprod.thy Fri May 27 00:16:18 2005 +0200 @@ -138,14 +138,14 @@ apply (rule contlubI [rule_format]) apply (subst thelub_cprod) apply (erule monofun_pair1 [THEN ch2ch_monofun]) -apply (simp add: lub_const [THEN thelubI]) +apply (simp add: thelub_const) done lemma contlub_pair2: "contlub (\y. (x, y))" apply (rule contlubI [rule_format]) apply (subst thelub_cprod) apply (erule monofun_pair2 [THEN ch2ch_monofun]) -apply (simp add: lub_const [THEN thelubI]) +apply (simp add: thelub_const) done lemma cont_pair1: "cont (\x. (x, y))"