src/HOLCF/Up.ML
changeset 19764 372065f34795
parent 19763 ec18656a2c10
child 19765 dfe940911617
--- a/src/HOLCF/Up.ML	Fri Jun 02 19:41:37 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-
-(* legacy ML bindings *)
-
-val antisym_less_up = thm "antisym_less_up";
-val compact_up = thm "compact_up";
-val cont_Ifup1 = thm "cont_Ifup1";
-val cont_Ifup2 = thm "cont_Ifup2";
-val cont_Iup = thm "cont_Iup";
-val cpo_up = thm "cpo_up";
-val Exh_Up = thm "Exh_Up";
-val fup1 = thm "fup1";
-val fup2 = thm "fup2";
-val fup3 = thm "fup3";
-val fup_def = thm "fup_def";
-val inst_up_pcpo = thm "inst_up_pcpo";
-val is_lub_Iup = thm "is_lub_Iup";
-val Iup_less = thm "Iup_less";
-val least_up = thm "least_up";
-val less_up_def = thm "less_up_def";
-val minimal_up = thm "minimal_up";
-val monofun_Ifup2 = thm "monofun_Ifup2";
-val not_Iup_less = thm "not_Iup_less";
-val not_up_less_UU = thm "not_up_less_UU";
-val refl_less_up = thm "refl_less_up";
-val trans_less_up = thm "trans_less_up";
-val up_chain_cases = thm "up_chain_cases";
-val up_defined = thm "up_defined";
-val up_def = thm "up_def";
-val up_eq = thm "up_eq";
-val upE = thm "upE";
-val up_inject = thm "up_inject";
-val up_lemma1 = thm "up_lemma1";
-val up_lemma2 = thm "up_lemma2";
-val up_lemma3 = thm "up_lemma3";
-val up_lemma4 = thm "up_lemma4";
-val up_lemma5 = thm "up_lemma5";
-val up_lemma6 = thm "up_lemma6";
-val up_less = thm "up_less";
-