src/HOLCF/HOLCF.thy

--- a/src/HOLCF/HOLCF.thy	Wed Oct 13 10:27:26 2010 -0700
+++ b/src/HOLCF/HOLCF.thy	Wed Oct 13 10:56:42 2010 -0700
@@ -23,6 +23,10 @@
 lemmas ext_cfun = cfun_eqI
 lemmas expand_cfun_below = cfun_below_iff
 lemmas below_cfun_ext = cfun_belowI
+lemmas monofun_fun_fun = fun_belowD
+lemmas monofun_fun_arg = monofunE
+lemmas monofun_lub_fun = adm_monofun [THEN admD]
+lemmas cont_lub_fun = adm_cont [THEN admD]
 
 text {* Older legacy theorem names: *}