| author | wenzelm |
| Wed, 13 Jul 2005 16:07:35 +0200 | |
| changeset 16813 | 67140ae50e77 |
| parent 16777 | 555c8951f05c |
| child 16922 | 2128ac2aa5db |
| 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 |
|
| 16699 | 4 |
val less_sprod_def = thm "less_Sprod_def"; |
|
15576
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"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
9 |
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
|
10 |
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
|
11 |
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
|
12 |
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
|
13 |
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
|
14 |
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
|
15 |
val spair_defined = thm "spair_defined"; |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
16 |
val spair_eq = thm "spair_eq"; |
|
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
17 |
val spair_inject = thm "spair_inject"; |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
18 |
val Exh_Sprod2 = thm "Exh_Sprod2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
19 |
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
|
20 |
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
|
21 |
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
|
22 |
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
|
23 |
val ssnd_spair = thm "ssnd_spair"; |
|
16777
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16699
diff
changeset
|
24 |
val sfst_defined = thm "sfst_defined"; |
|
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16699
diff
changeset
|
25 |
val ssnd_defined = thm "ssnd_defined"; |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
26 |
val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2"; |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
27 |
val less_sprod = thm "less_sprod"; |
|
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
28 |
val spair_less = thm "spair_less"; |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
29 |
val ssplit1 = thm "ssplit1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
30 |
val ssplit2 = thm "ssplit2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
31 |
val ssplit3 = thm "ssplit3"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
32 |