src/HOLCF/Up.ML
changeset 16753 fb6801c926d2
parent 16319 1ff2965cc2e7
child 16922 2128ac2aa5db
     1.1 --- a/src/HOLCF/Up.ML	Fri Jul 08 02:39:53 2005 +0200
     1.2 +++ b/src/HOLCF/Up.ML	Fri Jul 08 02:41:19 2005 +0200
     1.3 @@ -1,11 +1,7 @@
     1.4  
     1.5  (* legacy ML bindings *)
     1.6  
     1.7 -val Iup_def = thm "Iup_def";
     1.8 -val Ifup_def = thm "Ifup_def";
     1.9  val less_up_def = thm "less_up_def";
    1.10 -val Ifup1 = thm "Ifup1";
    1.11 -val Ifup2 = thm "Ifup2";
    1.12  val refl_less_up = thm "refl_less_up";
    1.13  val antisym_less_up = thm "antisym_less_up";
    1.14  val trans_less_up = thm "trans_less_up";
    1.15 @@ -20,12 +16,12 @@
    1.16  val cont_Iup = thm "cont_Iup";
    1.17  val cont_Ifup1 = thm "cont_Ifup1";
    1.18  val cont_Ifup2 = thm "cont_Ifup2";
    1.19 -val Exh_Up1 = thm "Exh_Up1";
    1.20 +val Exh_Up = thm "Exh_Up";
    1.21  val up_inject = thm "up_inject";
    1.22  val up_eq = thm "up_eq";
    1.23  val up_defined = thm "up_defined";
    1.24  val up_less = thm "up_less";
    1.25 -val upE1 = thm "upE1";
    1.26 +val upE = thm "upE";
    1.27  val fup1 = thm "fup1";
    1.28  val fup2 = thm "fup2";
    1.29  val fup3 = thm "fup3";