| author | huffman |
| Thu, 23 Jun 2005 22:10:29 +0200 | |
| changeset 16555 | cec3fbf9832b |
| parent 16316 | 17db5df51a35 |
| child 16699 | 24b494ff8f0f |
| permissions | -rw-r--r-- |
|
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]; |