src/HOLCF/Ffun.ML
changeset 16202 61811f31ce5a
child 16922 2128ac2aa5db
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Ffun.ML	Fri Jun 03 22:07:30 2005 +0200
@@ -0,0 +1,16 @@
+
+(* legacy ML bindings *)
+
+val less_fun_def = thm "less_fun_def";
+val refl_less_fun = thm "refl_less_fun";
+val antisym_less_fun = thm "antisym_less_fun";
+val trans_less_fun = thm "trans_less_fun";
+val minimal_fun = thm "minimal_fun";
+val least_fun = thm "least_fun";
+val less_fun = thm "less_fun";
+val ch2ch_fun = thm "ch2ch_fun";
+val ub2ub_fun = thm "ub2ub_fun";
+val lub_fun = thm "lub_fun";
+val thelub_fun = thm "thelub_fun";
+val cpo_fun = thm "cpo_fun";
+val inst_fun_pcpo = thm "inst_fun_pcpo";