src/HOLCF/Ssum.ML
author huffman
Sat, 04 Jun 2005 00:22:08 +0200
changeset 16221 879400e029bf
parent 16211 faa9691da2bc
child 16316 17db5df51a35
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 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";
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16060
diff changeset
    20
val sinl_defined = thm "sinl_defined";
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16060
diff changeset
    21
val sinr_defined = thm "sinr_defined";
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    22
val Exh_Ssum1 = thm "Exh_Ssum1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    23
val ssumE = thm "ssumE";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    24
val ssumE2 = thm "ssumE2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    25
val sscase1 = thm "sscase1";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    26
val sscase2 = thm "sscase2";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    27
val sscase3 = thm "sscase3";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    28
val less_ssum4a = thm "less_ssum4a";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    29
val less_ssum4b = thm "less_ssum4b";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    30
val less_ssum4c = thm "less_ssum4c";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    31
val less_ssum4d = thm "less_ssum4d";
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    32
val sscase4 = thm "sscase4";
16211
faa9691da2bc changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents: 16060
diff changeset
    33
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
    34
                sscase1, sscase2, sscase3];