src/HOLCF/Cprod.ML
author huffman
Tue, 26 Jul 2005 18:29:59 +0200
changeset 16922 2128ac2aa5db
parent 16210 5d1b752cacc1
child 17838 3032e90c4975
permissions -rw-r--r--
brought ML files up to date with new lemmas
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
16922
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
     4
val antisym_less_cprod = thm "antisym_less_cprod";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
     5
val cfst_cpair = thm "cfst_cpair";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
     6
val cfst_def = thm "cfst_def";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
     7
val cfst_strict = thm "cfst_strict";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
     8
val CLet_def = thm "CLet_def";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
     9
val cont_fst = thm "cont_fst";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    10
val contlub_fst = thm "contlub_fst";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    11
val contlub_pair1 = thm "contlub_pair1";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    12
val contlub_pair2 = thm "contlub_pair2";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    13
val contlub_snd = thm "contlub_snd";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    14
val cont_pair1 = thm "cont_pair1";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    15
val cont_pair2 = thm "cont_pair2";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    16
val cont_snd = thm "cont_snd";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    17
val cpair_def = thm "cpair_def";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    18
val cpair_defined_iff = thm "cpair_defined_iff";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    19
val cpair_eq_pair = thm "cpair_eq_pair";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    20
val cpair_eq = thm "cpair_eq";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    21
val cpair_less = thm "cpair_less";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    22
val cpo_cprod = thm "cpo_cprod";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    23
val cprodE = thm "cprodE";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    24
val Cprod_rews = thms "Cprod_rews";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    25
val csnd_cpair = thm "csnd_cpair";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    26
val csnd_def = thm "csnd_def";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    27
val csnd_strict = thm "csnd_strict";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    28
val csplit2 = thm "csplit2";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    29
val csplit3 = thm "csplit3";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    30
val csplit_def = thm "csplit_def";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    31
val defined_cpair_rev = thm "defined_cpair_rev";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    32
val eq_cprod = thm "eq_cprod";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    33
val Exh_Cprod2 = thm "Exh_Cprod2"; (* rename *)
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    34
val inject_cpair = thm "inject_cpair";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    35
val inst_cprod_pcpo2 = thm "inst_cprod_pcpo2"; (**)
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    36
val inst_cprod_pcpo = thm "inst_cprod_pcpo";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    37
val least_cprod = thm "least_cprod";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    38
val less_cprod_def = thm "less_cprod_def";
16922
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    39
val less_cprod = thm "less_cprod";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    40
val lub_cprod2 = thm "lub_cprod2"; (* *)
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    41
val lub_cprod = thm "lub_cprod";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    42
val minimal_cprod = thm "minimal_cprod";
16922
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    43
val monofun_fst = thm "monofun_fst";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    44
val monofun_pair1 = thm "monofun_pair1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    45
val monofun_pair2 = thm "monofun_pair2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    46
val monofun_pair = thm "monofun_pair";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    47
val monofun_snd = thm "monofun_snd";
16922
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    48
val refl_less_cprod = thm "refl_less_cprod";
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    49
val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2"; (* rename *)
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    50
val thelub_cprod2 = thm "thelub_cprod2"; (* *)
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    51
val thelub_cprod = thm "thelub_cprod";
16922
2128ac2aa5db brought ML files up to date with new lemmas
huffman
parents: 16210
diff changeset
    52
val trans_less_cprod = thm "trans_less_cprod";