| author | quigley |
| Mon, 23 May 2005 15:16:36 +0200 | |
| changeset 16048 | 25cb0fe2e1c6 |
| parent 15576 | efb95d0d01f7 |
| child 16059 | dab0d004732f |
| 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 Ispair_def = thm "Ispair_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
5 |
val Isfst_def = thm "Isfst_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
6 |
val Issnd_def = thm "Issnd_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
7 |
val SprodI = thm "SprodI"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
8 |
val inj_on_Abs_Sprod = thm "inj_on_Abs_Sprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
9 |
val strict_Spair_Rep = thm "strict_Spair_Rep"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
10 |
val defined_Spair_Rep_rev = thm "defined_Spair_Rep_rev"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
11 |
val inject_Spair_Rep = thm "inject_Spair_Rep"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
12 |
val inject_Ispair = thm "inject_Ispair"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
13 |
val strict_Ispair = thm "strict_Ispair"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
14 |
val strict_Ispair1 = thm "strict_Ispair1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
15 |
val strict_Ispair2 = thm "strict_Ispair2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
16 |
val strict_Ispair_rev = thm "strict_Ispair_rev"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
17 |
val defined_Ispair_rev = thm "defined_Ispair_rev"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
18 |
val defined_Ispair = thm "defined_Ispair"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
19 |
val Exh_Sprod = thm "Exh_Sprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
20 |
val IsprodE = thm "IsprodE"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
21 |
val strict_Isfst = thm "strict_Isfst"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
22 |
val strict_Isfst1 = thm "strict_Isfst1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
23 |
val strict_Isfst2 = thm "strict_Isfst2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
24 |
val strict_Issnd = thm "strict_Issnd"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
25 |
val strict_Issnd1 = thm "strict_Issnd1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
26 |
val strict_Issnd2 = thm "strict_Issnd2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
27 |
val Isfst = thm "Isfst"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
28 |
val Issnd = thm "Issnd"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
29 |
val Isfst2 = thm "Isfst2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
30 |
val Issnd2 = thm "Issnd2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
31 |
val Sprod0_ss = [strict_Isfst1, strict_Isfst2, strict_Issnd1, strict_Issnd2, |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
32 |
Isfst2, Issnd2] |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
33 |
val defined_IsfstIssnd = thm "defined_IsfstIssnd"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
34 |
val surjective_pairing_Sprod = thm "surjective_pairing_Sprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
35 |
val Sel_injective_Sprod = thm "Sel_injective_Sprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
36 |
val less_sprod_def = thm "less_sprod_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
37 |
val refl_less_sprod = thm "refl_less_sprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
38 |
val antisym_less_sprod = thm "antisym_less_sprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
39 |
val trans_less_sprod = thm "trans_less_sprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
40 |
val inst_sprod_po = thm "inst_sprod_po"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
41 |
val minimal_sprod = thm "minimal_sprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
42 |
val UU_sprod_def = thm "UU_sprod_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
43 |
val least_sprod = thm "least_sprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
44 |
val monofun_Ispair1 = thm "monofun_Ispair1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
45 |
val monofun_Ispair2 = thm "monofun_Ispair2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
46 |
val monofun_Ispair = thm "monofun_Ispair"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
47 |
val monofun_Isfst = thm "monofun_Isfst"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
48 |
val monofun_Issnd = thm "monofun_Issnd"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
49 |
val lub_sprod = thm "lub_sprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
50 |
val thelub_sprod = thm "thelub_sprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
51 |
val cpo_sprod = thm "cpo_sprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
52 |
val spair_def = thm "spair_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
53 |
val sfst_def = thm "sfst_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
54 |
val ssnd_def = thm "ssnd_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
55 |
val ssplit_def = thm "ssplit_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
56 |
val inst_sprod_pcpo = thm "inst_sprod_pcpo"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
57 |
val sprod3_lemma1 = thm "sprod3_lemma1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
58 |
val sprod3_lemma2 = thm "sprod3_lemma2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
59 |
val sprod3_lemma3 = thm "sprod3_lemma3"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
60 |
val contlub_Ispair1 = thm "contlub_Ispair1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
61 |
val sprod3_lemma4 = thm "sprod3_lemma4"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
62 |
val sprod3_lemma5 = thm "sprod3_lemma5"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
63 |
val sprod3_lemma6 = thm "sprod3_lemma6"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
64 |
val contlub_Ispair2 = thm "contlub_Ispair2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
65 |
val cont_Ispair1 = thm "cont_Ispair1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
66 |
val cont_Ispair2 = thm "cont_Ispair2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
67 |
val contlub_Isfst = thm "contlub_Isfst"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
68 |
val contlub_Issnd = thm "contlub_Issnd"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
69 |
val cont_Isfst = thm "cont_Isfst"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
70 |
val cont_Issnd = thm "cont_Issnd"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
71 |
val spair_eq = thm "spair_eq"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
72 |
val beta_cfun_sprod = thm "beta_cfun_sprod"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
73 |
val inject_spair = thm "inject_spair"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
74 |
val inst_sprod_pcpo2 = thm "inst_sprod_pcpo2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
75 |
val strict_spair = thm "strict_spair"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
76 |
val strict_spair1 = thm "strict_spair1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
77 |
val strict_spair2 = thm "strict_spair2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
78 |
val strict_spair_rev = thm "strict_spair_rev"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
79 |
val defined_spair_rev = thm "defined_spair_rev"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
80 |
val defined_spair = thm "defined_spair"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
81 |
val Exh_Sprod2 = thm "Exh_Sprod2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
82 |
val sprodE = thm "sprodE"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
83 |
val strict_sfst = thm "strict_sfst"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
84 |
val strict_sfst1 = thm "strict_sfst1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
85 |
val strict_sfst2 = thm "strict_sfst2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
86 |
val strict_ssnd = thm "strict_ssnd"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
87 |
val strict_ssnd1 = thm "strict_ssnd1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
88 |
val strict_ssnd2 = thm "strict_ssnd2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
89 |
val sfst2 = thm "sfst2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
90 |
val ssnd2 = thm "ssnd2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
91 |
val defined_sfstssnd = thm "defined_sfstssnd"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
92 |
val surjective_pairing_Sprod2 = thm "surjective_pairing_Sprod2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
93 |
val lub_sprod2 = thm "lub_sprod2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
94 |
val thelub_sprod2 = thm "thelub_sprod2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
95 |
val ssplit1 = thm "ssplit1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
96 |
val ssplit2 = thm "ssplit2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
97 |
val ssplit3 = thm "ssplit3"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
98 |
val Sprod_rews = [strict_sfst1, strict_sfst2, |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
99 |
strict_ssnd1, strict_ssnd2, sfst2, ssnd2, defined_spair, |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
100 |
ssplit1, ssplit2] |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
101 |