src/HOL/HOLCF/Cfun.thy
changeset 40834 a1249aeff5b6
parent 40794 d28d41ee4cef
child 41027 c599955d9806
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Tue Nov 30 15:34:51 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Tue Nov 30 15:56:19 2010 -0800
     1.3 @@ -192,7 +192,7 @@
     1.4  subsection {* Continuity of application *}
     1.5  
     1.6  lemma cont_Rep_cfun1: "cont (\<lambda>f. f\<cdot>x)"
     1.7 -by (rule cont_Rep_cfun [THEN cont2cont_fun])
     1.8 +by (rule cont_Rep_cfun [OF cont_id, THEN cont2cont_fun])
     1.9  
    1.10  lemma cont_Rep_cfun2: "cont (\<lambda>x. f\<cdot>x)"
    1.11  apply (cut_tac x=f in Rep_cfun)