src/HOL/HOLCF/HOLCF.thy
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