| author | huffman |
| Mon, 07 Mar 2005 23:30:06 +0100 | |
| changeset 15586 | f7f812034707 |
| parent 15576 | efb95d0d01f7 |
| child 15607 | 30576c645e91 |
| 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 Isinl_def = thm "Isinl_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
5 |
val Isinr_def = thm "Isinr_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
6 |
val Iwhen_def = thm "Iwhen_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
7 |
val SsumIl = thm "SsumIl"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
8 |
val SsumIr = thm "SsumIr"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
9 |
val inj_on_Abs_Ssum = thm "inj_on_Abs_Ssum"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
10 |
val strict_SinlSinr_Rep = thm "strict_SinlSinr_Rep"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
11 |
val strict_IsinlIsinr = thm "strict_IsinlIsinr"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
12 |
val noteq_SinlSinr_Rep = thm "noteq_SinlSinr_Rep"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
13 |
val noteq_IsinlIsinr = thm "noteq_IsinlIsinr"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
14 |
val inject_Sinl_Rep1 = thm "inject_Sinl_Rep1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
15 |
val inject_Sinr_Rep1 = thm "inject_Sinr_Rep1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
16 |
val inject_Sinl_Rep2 = thm "inject_Sinl_Rep2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
17 |
val inject_Sinr_Rep2 = thm "inject_Sinr_Rep2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
18 |
val inject_Sinl_Rep = thm "inject_Sinl_Rep"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
19 |
val inject_Sinr_Rep = thm "inject_Sinr_Rep"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
20 |
val inject_Isinl = thm "inject_Isinl"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
21 |
val inject_Isinr = thm "inject_Isinr"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
22 |
val inject_Isinl_rev = thm "inject_Isinl_rev"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
23 |
val inject_Isinr_rev = thm "inject_Isinr_rev"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
24 |
val Exh_Ssum = thm "Exh_Ssum"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
25 |
val IssumE = thm "IssumE"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
26 |
val IssumE2 = thm "IssumE2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
27 |
val Iwhen1 = thm "Iwhen1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
28 |
val Iwhen2 = thm "Iwhen2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
29 |
val Iwhen3 = thm "Iwhen3"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
30 |
val less_ssum_def = thm "less_ssum_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
31 |
val less_ssum1a = thm "less_ssum1a"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
32 |
val less_ssum1b = thm "less_ssum1b"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
33 |
val less_ssum1c = thm "less_ssum1c"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
34 |
val less_ssum1d = thm "less_ssum1d"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
35 |
val less_ssum2a = thm "less_ssum2a"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
36 |
val less_ssum2b = thm "less_ssum2b"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
37 |
val less_ssum2c = thm "less_ssum2c"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
38 |
val less_ssum2d = thm "less_ssum2d"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
39 |
val refl_less_ssum = thm "refl_less_ssum"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
40 |
val antisym_less_ssum = thm "antisym_less_ssum"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
41 |
val trans_less_ssum = thm "trans_less_ssum"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
42 |
val inst_ssum_po = thm "inst_ssum_po"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
43 |
val less_ssum3a = thm "less_ssum3a"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
44 |
val less_ssum3b = thm "less_ssum3b"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
45 |
val less_ssum3c = thm "less_ssum3c"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
46 |
val less_ssum3d = thm "less_ssum3d"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
47 |
val minimal_ssum = thm "minimal_ssum"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
48 |
val UU_ssum_def = thm "UU_ssum_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
49 |
val least_ssum = thm "least_ssum"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
50 |
val monofun_Isinl = thm "monofun_Isinl"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
51 |
val monofun_Isinr = thm "monofun_Isinr"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
52 |
val monofun_Iwhen1 = thm "monofun_Iwhen1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
53 |
val monofun_Iwhen2 = thm "monofun_Iwhen2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
54 |
val monofun_Iwhen3 = thm "monofun_Iwhen3"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
55 |
val ssum_lemma1 = thm "ssum_lemma1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
56 |
val ssum_lemma2 = thm "ssum_lemma2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
57 |
val ssum_lemma3 = thm "ssum_lemma3"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
58 |
val ssum_lemma4 = thm "ssum_lemma4"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
59 |
val ssum_lemma5 = thm "ssum_lemma5"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
60 |
val ssum_lemma6 = thm "ssum_lemma6"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
61 |
val ssum_lemma7 = thm "ssum_lemma7"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
62 |
val ssum_lemma8 = thm "ssum_lemma8"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
63 |
val lub_ssum1a = thm "lub_ssum1a"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
64 |
val lub_ssum1b = thm "lub_ssum1b"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
65 |
val thelub_ssum1a = thm "thelub_ssum1a"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
66 |
val thelub_ssum1b = thm "thelub_ssum1b"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
67 |
val cpo_ssum = thm "cpo_ssum"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
68 |
val sinl_def = thm "sinl_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
69 |
val sinr_def = thm "sinr_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
70 |
val sscase_def = thm "sscase_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
71 |
val inst_ssum_pcpo = thm "inst_ssum_pcpo"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
72 |
val contlub_Isinl = thm "contlub_Isinl"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
73 |
val contlub_Isinr = thm "contlub_Isinr"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
74 |
val cont_Isinl = thm "cont_Isinl"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
75 |
val cont_Isinr = thm "cont_Isinr"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
76 |
val contlub_Iwhen1 = thm "contlub_Iwhen1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
77 |
val contlub_Iwhen2 = thm "contlub_Iwhen2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
78 |
val ssum_lemma9 = thm "ssum_lemma9"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
79 |
val ssum_lemma10 = thm "ssum_lemma10"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
80 |
val ssum_lemma11 = thm "ssum_lemma11"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
81 |
val ssum_lemma12 = thm "ssum_lemma12"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
82 |
val ssum_lemma13 = thm "ssum_lemma13"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
83 |
val contlub_Iwhen3 = thm "contlub_Iwhen3"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
84 |
val cont_Iwhen1 = thm "cont_Iwhen1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
85 |
val cont_Iwhen2 = thm "cont_Iwhen2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
86 |
val cont_Iwhen3 = thm "cont_Iwhen3"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
87 |
val strict_sinl = thm "strict_sinl"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
88 |
val strict_sinr = thm "strict_sinr"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
89 |
val noteq_sinlsinr = thm "noteq_sinlsinr"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
90 |
val inject_sinl = thm "inject_sinl"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
91 |
val inject_sinr = thm "inject_sinr"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
92 |
val defined_sinl = thm "defined_sinl"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
93 |
val defined_sinr = thm "defined_sinr"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
94 |
val Exh_Ssum1 = thm "Exh_Ssum1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
95 |
val ssumE = thm "ssumE"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
96 |
val ssumE2 = thm "ssumE2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
97 |
val sscase1 = thm "sscase1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
98 |
val sscase2 = thm "sscase2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
99 |
val sscase3 = thm "sscase3"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
100 |
val less_ssum4a = thm "less_ssum4a"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
101 |
val less_ssum4b = thm "less_ssum4b"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
102 |
val less_ssum4c = thm "less_ssum4c"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
103 |
val less_ssum4d = thm "less_ssum4d"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
104 |
val ssum_chainE = thm "ssum_chainE"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
105 |
val thelub_ssum2a = thm "thelub_ssum2a"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
106 |
val thelub_ssum2b = thm "thelub_ssum2b"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
107 |
val thelub_ssum2a_rev = thm "thelub_ssum2a_rev"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
108 |
val thelub_ssum2b_rev = thm "thelub_ssum2b_rev"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
109 |
val thelub_ssum3 = thm "thelub_ssum3"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
110 |
val sscase4 = thm "sscase4"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
111 |
val Ssum_rews = [strict_sinl, strict_sinr, defined_sinl, defined_sinr, |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
112 |
sscase1, sscase2, sscase3] |