src/HOLCF/Ssum.ML
author huffman
Wed, 08 Jun 2005 00:16:28 +0200
changeset 16316 17db5df51a35
parent 16211 faa9691da2bc
child 16699 24b494ff8f0f
permissions -rw-r--r--
renamed theorems less_ssum4a,b,c,d to more meaningful names
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 Iwhen_def = thm "Iwhen_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     5
val Iwhen1 = thm "Iwhen1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     6
val Iwhen2 = thm "Iwhen2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     7
val Iwhen3 = thm "Iwhen3";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     8
val less_ssum_def = thm "less_ssum_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     9
val sinl_def = thm "sinl_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    10
val sinr_def = thm "sinr_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    11
val sscase_def = thm "sscase_def";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    12
val cont_Iwhen1 = thm "cont_Iwhen1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    13
val cont_Iwhen2 = thm "cont_Iwhen2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    14
val cont_Iwhen3 = thm "cont_Iwhen3";
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16060
diff changeset
    15
val sinl_strict = thm "sinl_strict";
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16060
diff changeset
    16
val sinr_strict = thm "sinr_strict";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    17
val noteq_sinlsinr = thm "noteq_sinlsinr";
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16060
diff changeset
    18
val sinl_inject = thm "sinl_inject";
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16060
diff changeset
    19
val sinr_inject = thm "sinr_inject";
16316
17db5df51a35 renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents: 16211
diff changeset
    20
val sinl_eq = thm "sinl_eq";
17db5df51a35 renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents: 16211
diff changeset
    21
val sinr_eq = thm "sinr_eq";
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16060
diff changeset
    22
val sinl_defined = thm "sinl_defined";
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16060
diff changeset
    23
val sinr_defined = thm "sinr_defined";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    24
val Exh_Ssum1 = thm "Exh_Ssum1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    25
val ssumE = thm "ssumE";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    26
val ssumE2 = thm "ssumE2";
16316
17db5df51a35 renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents: 16211
diff changeset
    27
val sinl_less = thm "sinl_less";
17db5df51a35 renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents: 16211
diff changeset
    28
val sinr_less = thm "sinr_less";
17db5df51a35 renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents: 16211
diff changeset
    29
val sinl_less_sinr = thm "sinl_less_sinr";
17db5df51a35 renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents: 16211
diff changeset
    30
val sinr_less_sinl = thm "sinr_less_sinl";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    31
val sscase1 = thm "sscase1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    32
val sscase2 = thm "sscase2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    33
val sscase3 = thm "sscase3";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    34
val sscase4 = thm "sscase4";
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16060
diff changeset
    35
val Ssum_rews = [sinl_strict, sinr_strict, sinl_defined, sinr_defined,
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16060
diff changeset
    36
                sscase1, sscase2, sscase3];