src/HOLCF/Up.ML
author huffman
Fri Jul 08 02:41:19 2005 +0200 (2005-07-08)
changeset 16753 fb6801c926d2
parent 16319 1ff2965cc2e7
child 16922 2128ac2aa5db
permissions -rw-r--r--
define 'a u with datatype package;
removed obsolete lemmas;
renamed upE1 to upE and Exh_Up1 to Exh_Up;
cleaned up
huffman@15576
     1
huffman@15576
     2
(* legacy ML bindings *)
huffman@15576
     3
huffman@15576
     4
val less_up_def = thm "less_up_def";
huffman@15576
     5
val refl_less_up = thm "refl_less_up";
huffman@15576
     6
val antisym_less_up = thm "antisym_less_up";
huffman@15576
     7
val trans_less_up = thm "trans_less_up";
huffman@15576
     8
val minimal_up = thm "minimal_up";
huffman@15576
     9
val least_up = thm "least_up";
huffman@15576
    10
val monofun_Ifup2 = thm "monofun_Ifup2";
huffman@15576
    11
val up_lemma1 = thm "up_lemma1";
huffman@15576
    12
val cpo_up = thm "cpo_up";
huffman@15576
    13
val up_def = thm "up_def";
huffman@15576
    14
val fup_def = thm "fup_def";
huffman@15576
    15
val inst_up_pcpo = thm "inst_up_pcpo";
huffman@15576
    16
val cont_Iup = thm "cont_Iup";
huffman@15576
    17
val cont_Ifup1 = thm "cont_Ifup1";
huffman@15576
    18
val cont_Ifup2 = thm "cont_Ifup2";
huffman@16753
    19
val Exh_Up = thm "Exh_Up";
huffman@16319
    20
val up_inject = thm "up_inject";
huffman@16319
    21
val up_eq = thm "up_eq";
huffman@16319
    22
val up_defined = thm "up_defined";
huffman@16319
    23
val up_less = thm "up_less";
huffman@16753
    24
val upE = thm "upE";
huffman@15576
    25
val fup1 = thm "fup1";
huffman@15576
    26
val fup2 = thm "fup2";
huffman@15576
    27
val fup3 = thm "fup3";