--- a/src/HOLCF/Porder.ML Fri Mar 04 18:53:46 2005 +0100
+++ b/src/HOLCF/Porder.ML Fri Mar 04 23:12:36 2005 +0100
@@ -1,6 +1,13 @@
(* legacy ML bindings *)
+val refl_less = thm "refl_less";
+val antisym_less = thm "antisym_less";
+val trans_less = thm "trans_less";
+val minimal2UU = thm "minimal2UU";
+val antisym_less_inverse = thm "antisym_less_inverse";
+val box_less = thm "box_less";
+val po_eq_conv = thm "po_eq_conv";
val is_ub_def = thm "is_ub_def";
val is_lub_def = thm "is_lub_def";
val tord_def = thm "tord_def";