src/HOLCF/Up.ML
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 15576 efb95d0d01f7
child 16319 1ff2965cc2e7
permissions -rw-r--r--
New theory with lemmas for the fixrec package
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     1
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     2
(* legacy ML bindings *)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     3
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     4
val Iup_def = thm "Iup_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     5
val Ifup_def = thm "Ifup_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     6
val less_up_def = thm "less_up_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     7
val Abs_Up_inverse2 = thm "Abs_Up_inverse2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     8
val Exh_Up = thm "Exh_Up";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     9
val inj_Abs_Up = thm "inj_Abs_Up";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    10
val inj_Rep_Up = thm "inj_Rep_Up";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    11
val inject_Iup = thm "inject_Iup";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    12
val defined_Iup = thm "defined_Iup";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    13
val upE = thm "upE";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    14
val Ifup1 = thm "Ifup1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    15
val Ifup2 = thm "Ifup2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    16
val less_up1a = thm "less_up1a";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    17
val less_up1b = thm "less_up1b";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    18
val less_up1c = thm "less_up1c";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    19
val refl_less_up = thm "refl_less_up";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    20
val antisym_less_up = thm "antisym_less_up";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    21
val trans_less_up = thm "trans_less_up";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    22
val inst_up_po = thm "inst_up_po";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    23
val minimal_up = thm "minimal_up";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    24
val UU_up_def = thm "UU_up_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    25
val least_up = thm "least_up";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    26
val less_up2b = thm "less_up2b";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    27
val less_up2c = thm "less_up2c";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    28
val monofun_Iup = thm "monofun_Iup";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    29
val monofun_Ifup1 = thm "monofun_Ifup1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    30
val monofun_Ifup2 = thm "monofun_Ifup2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    31
val up_lemma1 = thm "up_lemma1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    32
val lub_up1a = thm "lub_up1a";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    33
val lub_up1b = thm "lub_up1b";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    34
val thelub_up1a = thm "thelub_up1a";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    35
val thelub_up1b = thm "thelub_up1b";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    36
val cpo_up = thm "cpo_up";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    37
val up_def = thm "up_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    38
val fup_def = thm "fup_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    39
val inst_up_pcpo = thm "inst_up_pcpo";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    40
val less_up3b = thm "less_up3b";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    41
val defined_Iup2 = thm "defined_Iup2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    42
val contlub_Iup = thm "contlub_Iup";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    43
val cont_Iup = thm "cont_Iup";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    44
val contlub_Ifup1 = thm "contlub_Ifup1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    45
val contlub_Ifup2 = thm "contlub_Ifup2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    46
val cont_Ifup1 = thm "cont_Ifup1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    47
val cont_Ifup2 = thm "cont_Ifup2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    48
val Exh_Up1 = thm "Exh_Up1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    49
val inject_up = thm "inject_up";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    50
val defined_up = thm "defined_up";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    51
val upE1 = thm "upE1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    52
val fup1 = thm "fup1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    53
val fup2 = thm "fup2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    54
val less_up4b = thm "less_up4b";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    55
val less_up4c = thm "less_up4c";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    56
val thelub_up2a = thm "thelub_up2a";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    57
val thelub_up2b = thm "thelub_up2b";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    58
val up_lemma2 = thm "up_lemma2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    59
val thelub_up2a_rev = thm "thelub_up2a_rev";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    60
val thelub_up2b_rev = thm "thelub_up2b_rev";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    61
val thelub_up3 = thm "thelub_up3";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    62
val fup3 = thm "fup3";