| changeset 39974 | b525988432e9 |
| parent 37111 | 3f84f1f4de64 |
| child 40002 | c5b5f7a3a3b1 |
--- a/src/HOLCF/HOLCF.thy Tue Oct 05 17:53:00 2010 -0700 +++ b/src/HOLCF/HOLCF.thy Wed Oct 06 10:49:27 2010 -0700 @@ -45,8 +45,6 @@ lemmas expand_cfun_less = expand_cfun_below lemmas less_cfun_ext = below_cfun_ext lemmas injection_less = injection_below -lemmas approx_less = approx_below -lemmas profinite_less_ext = profinite_below_ext lemmas less_up_def = below_up_def lemmas not_Iup_less = not_Iup_below lemmas Iup_less = Iup_below