| changeset 16388 | 1ff571813848 |
| parent 16204 | 5dd79d3f0105 |
| child 16625 | 53d4e0f2839b |
--- a/src/HOLCF/Cont.ML Tue Jun 14 04:04:09 2005 +0200 +++ b/src/HOLCF/Cont.ML Tue Jun 14 04:05:15 2005 +0200 @@ -24,6 +24,7 @@ val cont2cont_CF1L = thm "cont2cont_CF1L"; val mono2mono_MF1L_rev = thm "mono2mono_MF1L_rev"; val cont2cont_CF1L_rev = thm "cont2cont_CF1L_rev"; +val cont2cont_lambda = thm "cont2cont_lambda"; val contlub_abstraction = thm "contlub_abstraction"; val mono2mono_app = thm "mono2mono_app"; val cont2contlub_app = thm "cont2contlub_app";