src/HOL/HOLCF/Cfun.thy
changeset 45606 b1e1508643b1
parent 42284 326f57825e1a
child 45695 b108b3d7c49e
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Sun Nov 20 21:05:23 2011 +0100
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Sun Nov 20 21:07:06 2011 +0100
     1.3 @@ -194,8 +194,8 @@
     1.4  
     1.5  lemmas monofun_Rep_cfun = cont_Rep_cfun [THEN cont2mono]
     1.6  
     1.7 -lemmas monofun_Rep_cfun1 = cont_Rep_cfun1 [THEN cont2mono, standard]
     1.8 -lemmas monofun_Rep_cfun2 = cont_Rep_cfun2 [THEN cont2mono, standard]
     1.9 +lemmas monofun_Rep_cfun1 = cont_Rep_cfun1 [THEN cont2mono]
    1.10 +lemmas monofun_Rep_cfun2 = cont_Rep_cfun2 [THEN cont2mono]
    1.11  
    1.12  text {* contlub, cont properties of @{term Rep_cfun} in each argument *}
    1.13