| author | wenzelm |
| Tue, 17 May 2005 09:58:40 +0200 | |
| changeset 15967 | f9163c6f69d6 |
| parent 15592 | 40088b01f257 |
| child 16081 | 81a4b4a245b0 |
| 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 less_cprod_def = thm "less_cprod_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
5 |
val refl_less_cprod = thm "refl_less_cprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
6 |
val antisym_less_cprod = thm "antisym_less_cprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
7 |
val trans_less_cprod = thm "trans_less_cprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
8 |
val inst_cprod_po = thm "inst_cprod_po"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
9 |
val less_cprod4c = thm "less_cprod4c"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
10 |
val minimal_cprod = thm "minimal_cprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
11 |
val UU_cprod_def = thm "UU_cprod_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
12 |
val least_cprod = thm "least_cprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
13 |
val monofun_pair1 = thm "monofun_pair1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
14 |
val monofun_pair2 = thm "monofun_pair2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
15 |
val monofun_pair = thm "monofun_pair"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
16 |
val monofun_fst = thm "monofun_fst"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
17 |
val monofun_snd = thm "monofun_snd"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
18 |
val lub_cprod = thm "lub_cprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
19 |
val thelub_cprod = thm "thelub_cprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
20 |
val cpo_cprod = thm "cpo_cprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
21 |
val cpair_def = thm "cpair_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
22 |
val cfst_def = thm "cfst_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
23 |
val csnd_def = thm "csnd_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
24 |
val csplit_def = thm "csplit_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
25 |
val CLet_def = thm "CLet_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
26 |
val inst_cprod_pcpo = thm "inst_cprod_pcpo"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
27 |
val contlub_pair1 = thm "contlub_pair1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
28 |
val contlub_pair2 = thm "contlub_pair2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
29 |
val cont_pair1 = thm "cont_pair1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
30 |
val cont_pair2 = thm "cont_pair2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
31 |
val contlub_fst = thm "contlub_fst"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
32 |
val contlub_snd = thm "contlub_snd"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
33 |
val cont_fst = thm "cont_fst"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
34 |
val cont_snd = thm "cont_snd"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
35 |
val beta_cfun_cprod = thm "beta_cfun_cprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
36 |
val inject_cpair = thm "inject_cpair"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
37 |
val inst_cprod_pcpo2 = thm "inst_cprod_pcpo2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
38 |
val defined_cpair_rev = thm "defined_cpair_rev"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
39 |
val Exh_Cprod2 = thm "Exh_Cprod2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
40 |
val cprodE = thm "cprodE"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
41 |
val cfst2 = thm "cfst2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
42 |
val csnd2 = thm "csnd2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
43 |
val cfst_strict = thm "cfst_strict"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
44 |
val csnd_strict = thm "csnd_strict"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
45 |
val surjective_pairing_Cprod2 = thm "surjective_pairing_Cprod2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
46 |
val less_cprod5c = thm "less_cprod5c"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
47 |
val lub_cprod2 = thm "lub_cprod2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
48 |
val thelub_cprod2 = thm "thelub_cprod2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
49 |
val csplit2 = thm "csplit2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
50 |
val csplit3 = thm "csplit3"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
51 |
val Cprod_rews = [cfst2, csnd2, csplit2] |