src/HOLCF/Sprod.ML
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 16212 422f836f6b39
child 16317 868eddbcaf6e
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 less_sprod_def = thm "less_sprod_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     5
val spair_def = thm "spair_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     6
val sfst_def = thm "sfst_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     7
val ssnd_def = thm "ssnd_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     8
val ssplit_def = thm "ssplit_def";
16212
422f836f6b39 renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents: 16059
diff changeset
     9
val spair_inject = thm "spair_inject";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    10
val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2";
16212
422f836f6b39 renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents: 16059
diff changeset
    11
val spair_strict = thm "spair_strict";
422f836f6b39 renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents: 16059
diff changeset
    12
val spair_strict1 = thm "spair_strict1";
422f836f6b39 renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents: 16059
diff changeset
    13
val spair_strict2 = thm "spair_strict2";
422f836f6b39 renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents: 16059
diff changeset
    14
val spair_strict_rev = thm "spair_strict_rev";
422f836f6b39 renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents: 16059
diff changeset
    15
val spair_defined_rev = thm "spair_defined_rev";
422f836f6b39 renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents: 16059
diff changeset
    16
val spair_defined = thm "spair_defined";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    17
val Exh_Sprod2 = thm "Exh_Sprod2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    18
val sprodE = thm "sprodE";
16212
422f836f6b39 renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents: 16059
diff changeset
    19
val sfst_strict = thm "sfst_strict";
422f836f6b39 renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents: 16059
diff changeset
    20
val ssnd_strict = thm "ssnd_strict";
422f836f6b39 renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents: 16059
diff changeset
    21
val sfst_spair = thm "sfst_spair";
422f836f6b39 renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents: 16059
diff changeset
    22
val ssnd_spair = thm "ssnd_spair";
422f836f6b39 renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents: 16059
diff changeset
    23
val sfstssnd_defined = thm "sfstssnd_defined";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    24
val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    25
val ssplit1 = thm "ssplit1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    26
val ssplit2 = thm "ssplit2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    27
val ssplit3 = thm "ssplit3";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    28