changeset 41027 | c599955d9806 |
parent 40774 | 0437dbc127b3 |
child 41414 | 00b2b6716ed8 |
--- a/src/HOL/HOLCF/HOLCF.thy Mon Dec 06 13:46:45 2010 +0100 +++ b/src/HOL/HOLCF/HOLCF.thy Mon Dec 06 08:30:00 2010 -0800 @@ -32,8 +32,8 @@ lemmas cont_Rep_CFun_app_app = cont_APP_app_app lemmas cont_cfun_fun = cont_Rep_cfun1 [THEN contE] lemmas cont_cfun_arg = cont_Rep_cfun2 [THEN contE] -(* +lemmas contlub_cfun = lub_APP [symmetric] +lemmas contlub_LAM = lub_LAM [symmetric] lemmas thelubI = lub_eqI -*) end