src/HOLCF/Cont.ML
changeset 18092 2c5d5da79a1e
parent 16922 2128ac2aa5db
--- a/src/HOLCF/Cont.ML	Sat Nov 05 21:42:24 2005 +0100
+++ b/src/HOLCF/Cont.ML	Sat Nov 05 21:50:37 2005 +0100
@@ -8,8 +8,7 @@
 val cont2cont_app2 = thm "cont2cont_app2";
 val cont2cont_app3 = thm "cont2cont_app3";
 val cont2cont_app = thm "cont2cont_app";
-val cont2cont_CF1L_rev = thm "cont2cont_CF1L_rev";
-val cont2cont_CF1L = thm "cont2cont_CF1L";
+val cont2cont_fun = thm "cont2cont_fun";
 val cont2cont_lambda = thm "cont2cont_lambda";
 val cont2contlub_app = thm "cont2contlub_app";
 val cont2contlubE = thm "cont2contlubE";
@@ -31,8 +30,8 @@
 val flatdom_strict2cont = thm "flatdom_strict2cont";
 val flatdom_strict2mono = thm "flatdom_strict2mono";
 val mono2mono_app = thm "mono2mono_app";
-val mono2mono_MF1L_rev = thm "mono2mono_MF1L_rev";
-val mono2mono_MF1L = thm "mono2mono_MF1L";
+val mono2mono_fun = thm "mono2mono_fun";
+val mono2mono_lambda = thm "mono2mono_lambda";
 val monocontlub2cont = thm "monocontlub2cont";
 val monofun_def = thm "monofun_def";
 val monofunE = thm "monofunE";