| author | huffman |
| Fri, 03 Jun 2005 23:23:55 +0200 | |
| changeset 16209 | 36ee7f6af79f |
| parent 16099 | c5882ca551dd |
| child 16314 | 7102a1aaecfd |
| 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_cfun_def = thm "less_cfun_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
5 |
val cfun_cong = thm "cfun_cong"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
6 |
val cfun_fun_cong = thm "cfun_fun_cong"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
7 |
val cfun_arg_cong = thm "cfun_arg_cong"; |
|
16209
36ee7f6af79f
removed dependencies on MF2 lemmas; removed some obsolete theorems; cleaned up many proofs; renamed less_cfun2 to less_cfun_ext
huffman
parents:
16099
diff
changeset
|
8 |
val Abs_CFun_inverse2 = thm "Abs_CFun_inverse2"; |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
9 |
val beta_cfun = thm "beta_cfun"; |
| 15641 | 10 |
val eta_cfun = thm "eta_cfun"; |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
11 |
val cont_Rep_CFun2 = thm "cont_Rep_CFun2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
12 |
val monofun_Rep_CFun2 = thm "monofun_Rep_CFun2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
13 |
val contlub_Rep_CFun2 = thm "contlub_Rep_CFun2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
14 |
val cont_cfun_arg = thm "cont_cfun_arg"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
15 |
val contlub_cfun_arg = thm "contlub_cfun_arg"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
16 |
val monofun_Rep_CFun1 = thm "monofun_Rep_CFun1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
17 |
val monofun_cfun_fun = thm "monofun_cfun_fun"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
18 |
val monofun_cfun_arg = thm "monofun_cfun_arg"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
19 |
val chain_monofun = thm "chain_monofun"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
20 |
val monofun_cfun = thm "monofun_cfun"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
21 |
val strictI = thm "strictI"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
22 |
val ch2ch_Rep_CFunR = thm "ch2ch_Rep_CFunR"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
23 |
val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
24 |
val lub_cfun_mono = thm "lub_cfun_mono"; |
|
16209
36ee7f6af79f
removed dependencies on MF2 lemmas; removed some obsolete theorems; cleaned up many proofs; renamed less_cfun2 to less_cfun_ext
huffman
parents:
16099
diff
changeset
|
25 |
val ex_lub_cfun = thm "ex_lub_cfun"; |
|
36ee7f6af79f
removed dependencies on MF2 lemmas; removed some obsolete theorems; cleaned up many proofs; renamed less_cfun2 to less_cfun_ext
huffman
parents:
16099
diff
changeset
|
26 |
val cont_lub_cfun = thm "cont_lub_cfun"; |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
27 |
val lub_cfun = thm "lub_cfun"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
28 |
val thelub_cfun = thm "thelub_cfun"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
29 |
val ext_cfun = thm "ext_cfun"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
30 |
val semi_monofun_Abs_CFun = thm "semi_monofun_Abs_CFun"; |
|
16209
36ee7f6af79f
removed dependencies on MF2 lemmas; removed some obsolete theorems; cleaned up many proofs; renamed less_cfun2 to less_cfun_ext
huffman
parents:
16099
diff
changeset
|
31 |
val less_cfun_ext = thm "less_cfun_ext"; |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
32 |
val Istrictify_def = thm "Istrictify_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
33 |
val strictify_def = thm "strictify_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
34 |
val ID_def = thm "ID_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
35 |
val oo_def = thm "oo_def"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
36 |
val inst_cfun_pcpo = thm "inst_cfun_pcpo"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
37 |
val contlub_Rep_CFun1 = thm "contlub_Rep_CFun1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
38 |
val cont_Rep_CFun1 = thm "cont_Rep_CFun1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
39 |
val contlub_cfun_fun = thm "contlub_cfun_fun"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
40 |
val cont_cfun_fun = thm "cont_cfun_fun"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
41 |
val contlub_cfun = thm "contlub_cfun"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
42 |
val cont_cfun = thm "cont_cfun"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
43 |
val cont2cont_Rep_CFun = thm "cont2cont_Rep_CFun"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
44 |
val cont2mono_LAM = thm "cont2mono_LAM"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
45 |
val cont2cont_LAM = thm "cont2cont_LAM"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
46 |
val cont_lemmas1 = [cont_const, cont_id, cont_Rep_CFun2, |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
47 |
cont2cont_Rep_CFun, cont2cont_LAM]; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
48 |
val Istrictify1 = thm "Istrictify1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
49 |
val Istrictify2 = thm "Istrictify2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
50 |
val monofun_Istrictify2 = thm "monofun_Istrictify2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
51 |
val contlub_Istrictify2 = thm "contlub_Istrictify2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
52 |
val cont_Istrictify1 = thm "cont_Istrictify1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
53 |
val cont_Istrictify2 = thm "cont_Istrictify2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
54 |
val strictify1 = thm "strictify1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
55 |
val strictify2 = thm "strictify2"; |
|
16209
36ee7f6af79f
removed dependencies on MF2 lemmas; removed some obsolete theorems; cleaned up many proofs; renamed less_cfun2 to less_cfun_ext
huffman
parents:
16099
diff
changeset
|
56 |
val Rep_CFun_strict1 = thm "Rep_CFun_strict1"; |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
57 |
val chfin_Rep_CFunR = thm "chfin_Rep_CFunR"; |
|
16085
c004b9bc970e
rewrote continuous isomorphism section, cleaned up
huffman
parents:
15641
diff
changeset
|
58 |
val retraction_strict = thm "retraction_strict"; |
|
c004b9bc970e
rewrote continuous isomorphism section, cleaned up
huffman
parents:
15641
diff
changeset
|
59 |
val injection_eq = thm "injection_eq"; |
|
c004b9bc970e
rewrote continuous isomorphism section, cleaned up
huffman
parents:
15641
diff
changeset
|
60 |
val injection_defined_rev = thm "injection_defined_rev"; |
|
c004b9bc970e
rewrote continuous isomorphism section, cleaned up
huffman
parents:
15641
diff
changeset
|
61 |
val injection_defined = thm "injection_defined"; |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
62 |
val chfin2chfin = thm "chfin2chfin"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
63 |
val flat2flat = thm "flat2flat"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
64 |
val flat_codom = thm "flat_codom"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
65 |
val ID1 = thm "ID1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
66 |
val cfcomp1 = thm "cfcomp1"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
67 |
val cfcomp2 = thm "cfcomp2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
68 |
val ID2 = thm "ID2"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
69 |
val ID3 = thm "ID3"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
70 |
val assoc_oo = thm "assoc_oo"; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
71 |
|
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
72 |
structure Cfun = |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
73 |
struct |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
74 |
val thy = the_context (); |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
75 |
val Istrictify_def = Istrictify_def; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
76 |
val strictify_def = strictify_def; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
77 |
val ID_def = ID_def; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
78 |
val oo_def = oo_def; |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
79 |
end; |