src/HOLCF/Cprod.ML
author huffman
Fri, 04 Mar 2005 23:12:36 +0100
changeset 15576 efb95d0d01f7
child 15592 40088b01f257
permissions -rw-r--r--
converted to new-style theories, and combined numbered files
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 less_cprod_def = thm "less_cprod_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     5
val refl_less_cprod = thm "refl_less_cprod";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     6
val antisym_less_cprod = thm "antisym_less_cprod";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     7
val trans_less_cprod = thm "trans_less_cprod";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     8
val inst_cprod_po = thm "inst_cprod_po";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     9
val less_cprod4c = thm "less_cprod4c";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    10
val minimal_cprod = thm "minimal_cprod";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    11
val UU_cprod_def = thm "UU_cprod_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    12
val least_cprod = thm "least_cprod";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    13
val monofun_pair1 = thm "monofun_pair1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    14
val monofun_pair2 = thm "monofun_pair2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    15
val monofun_pair = thm "monofun_pair";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    16
val monofun_fst = thm "monofun_fst";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    17
val monofun_snd = thm "monofun_snd";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    18
val lub_cprod = thm "lub_cprod";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    19
val thelub_cprod = thm "thelub_cprod";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    20
val cpo_cprod = thm "cpo_cprod";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    21
val cpair_def = thm "cpair_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    22
val cfst_def = thm "cfst_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    23
val csnd_def = thm "csnd_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    24
val csplit_def = thm "csplit_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    25
val CLet_def = thm "CLet_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    26
val inst_cprod_pcpo = thm "inst_cprod_pcpo";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    27
val Cprod3_lemma1 = thm "Cprod3_lemma1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    28
val contlub_pair1 = thm "contlub_pair1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    29
val Cprod3_lemma2 = thm "Cprod3_lemma2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    30
val contlub_pair2 = thm "contlub_pair2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    31
val cont_pair1 = thm "cont_pair1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    32
val cont_pair2 = thm "cont_pair2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    33
val contlub_fst = thm "contlub_fst";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    34
val contlub_snd = thm "contlub_snd";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    35
val cont_fst = thm "cont_fst";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    36
val cont_snd = thm "cont_snd";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    37
val beta_cfun_cprod = thm "beta_cfun_cprod";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    38
val inject_cpair = thm "inject_cpair";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    39
val inst_cprod_pcpo2 = thm "inst_cprod_pcpo2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    40
val defined_cpair_rev = thm "defined_cpair_rev";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    41
val Exh_Cprod2 = thm "Exh_Cprod2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    42
val cprodE = thm "cprodE";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    43
val cfst2 = thm "cfst2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    44
val csnd2 = thm "csnd2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    45
val cfst_strict = thm "cfst_strict";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    46
val csnd_strict = thm "csnd_strict";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    47
val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    48
val less_cprod5c = thm "less_cprod5c";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    49
val lub_cprod2 = thm "lub_cprod2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    50
val thelub_cprod2 = thm "thelub_cprod2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    51
val csplit2 = thm "csplit2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    52
val csplit3 = thm "csplit3";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    53
val Cprod_rews = [cfst2, csnd2, csplit2]