1 |
1 |
2 (* legacy ML bindings *) |
2 (* legacy ML bindings *) |
3 |
3 |
4 val less_cfun_def = thm "less_CFun_def"; |
4 val Abs_CFun_inverse2 = thm "Abs_CFun_inverse2"; |
|
5 val adm_cont = thm "adm_cont"; |
|
6 val assoc_oo = thm "assoc_oo"; |
|
7 val beta_cfun = thm "beta_cfun"; |
|
8 val cfcomp1 = thm "cfcomp1"; |
|
9 val cfcomp2 = thm "cfcomp2"; |
|
10 val cfun_arg_cong = thm "cfun_arg_cong"; |
5 val cfun_cong = thm "cfun_cong"; |
11 val cfun_cong = thm "cfun_cong"; |
6 val cfun_fun_cong = thm "cfun_fun_cong"; |
12 val cfun_fun_cong = thm "cfun_fun_cong"; |
7 val cfun_arg_cong = thm "cfun_arg_cong"; |
13 val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL"; |
8 val Abs_CFun_inverse2 = thm "Abs_CFun_inverse2"; |
14 val ch2ch_Rep_CFunR = thm "ch2ch_Rep_CFunR"; |
9 val beta_cfun = thm "beta_cfun"; |
15 val ch2ch_Rep_CFun = thm "ch2ch_Rep_CFun"; |
10 val eta_cfun = thm "eta_cfun"; |
|
11 val cont_Rep_CFun2 = thm "cont_Rep_CFun2"; |
|
12 val monofun_Rep_CFun2 = thm "monofun_Rep_CFun2"; |
|
13 val contlub_Rep_CFun2 = thm "contlub_Rep_CFun2"; |
|
14 val cont_cfun_arg = thm "cont_cfun_arg"; |
|
15 val contlub_cfun_arg = thm "contlub_cfun_arg"; |
|
16 val monofun_Rep_CFun1 = thm "monofun_Rep_CFun1"; |
|
17 val monofun_cfun_fun = thm "monofun_cfun_fun"; |
|
18 val monofun_cfun_arg = thm "monofun_cfun_arg"; |
|
19 val chain_monofun = thm "chain_monofun"; |
16 val chain_monofun = thm "chain_monofun"; |
20 val monofun_cfun = thm "monofun_cfun"; |
17 val chfin2chfin = thm "chfin2chfin"; |
21 val strictI = thm "strictI"; |
18 val chfin_Rep_CFunR = thm "chfin_Rep_CFunR"; |
22 val ch2ch_Rep_CFunR = thm "ch2ch_Rep_CFunR"; |
19 val cont2cont_LAM = thm "cont2cont_LAM"; |
23 val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL"; |
|
24 val lub_cfun_mono = thm "lub_cfun_mono"; |
|
25 val ex_lub_cfun = thm "ex_lub_cfun"; |
|
26 val cont_lub_cfun = thm "cont_lub_cfun"; |
|
27 val lub_cfun = thm "lub_cfun"; |
|
28 val thelub_cfun = thm "thelub_cfun"; |
|
29 val ext_cfun = thm "ext_cfun"; |
|
30 val semi_monofun_Abs_CFun = thm "semi_monofun_Abs_CFun"; |
|
31 val less_cfun_ext = thm "less_cfun_ext"; |
|
32 val Istrictify_def = thm "Istrictify_def"; |
|
33 val strictify_def = thm "strictify_def"; |
|
34 val ID_def = thm "ID_def"; |
|
35 val oo_def = thm "oo_def"; |
|
36 val inst_cfun_pcpo = thm "inst_cfun_pcpo"; |
|
37 val contlub_Rep_CFun1 = thm "contlub_Rep_CFun1"; |
|
38 val cont_Rep_CFun1 = thm "cont_Rep_CFun1"; |
|
39 val contlub_cfun_fun = thm "contlub_cfun_fun"; |
|
40 val cont_cfun_fun = thm "cont_cfun_fun"; |
|
41 val contlub_cfun = thm "contlub_cfun"; |
|
42 val cont_cfun = thm "cont_cfun"; |
|
43 val cont2cont_Rep_CFun = thm "cont2cont_Rep_CFun"; |
20 val cont2cont_Rep_CFun = thm "cont2cont_Rep_CFun"; |
44 val cont2mono_LAM = thm "cont2mono_LAM"; |
21 val cont2mono_LAM = thm "cont2mono_LAM"; |
45 val cont2cont_LAM = thm "cont2cont_LAM"; |
22 val cont_cfun_arg = thm "cont_cfun_arg"; |
46 val cont_lemmas1 = [cont_const, cont_id, cont_Rep_CFun2, |
23 val cont_cfun_fun = thm "cont_cfun_fun"; |
47 cont2cont_Rep_CFun, cont2cont_LAM]; |
24 val cont_cfun = thm "cont_cfun"; |
|
25 val cont_Istrictify1 = thm "cont_Istrictify1"; |
|
26 val cont_Istrictify2 = thm "cont_Istrictify2"; |
|
27 val cont_lemmas1 = thms "cont_lemmas1"; |
|
28 val contlub_cfun_arg = thm "contlub_cfun_arg"; |
|
29 val contlub_cfun_fun = thm "contlub_cfun_fun"; |
|
30 val cont_lub_cfun = thm "cont_lub_cfun"; |
|
31 val contlub_cfun = thm "contlub_cfun"; |
|
32 val contlub_Istrictify2 = thm "contlub_Istrictify2"; |
|
33 val contlub_Rep_CFun1 = thm "contlub_Rep_CFun1"; |
|
34 val contlub_Rep_CFun2 = thm "contlub_Rep_CFun2"; |
|
35 val cont_Rep_CFun1 = thm "cont_Rep_CFun1"; |
|
36 val cont_Rep_CFun2 = thm "cont_Rep_CFun2"; |
|
37 val eta_cfun = thm "eta_cfun"; |
|
38 val ex_lub_cfun = thm "ex_lub_cfun"; |
|
39 val ext_cfun = thm "ext_cfun"; |
|
40 val flat2flat = thm "flat2flat"; |
|
41 val flat_codom = thm "flat_codom"; |
|
42 val flat_eqI = thm "flat_eqI"; |
|
43 val ID1 = thm "ID1"; |
|
44 val ID2 = thm "ID2"; |
|
45 val ID3 = thm "ID3"; |
|
46 val ID_def = thm "ID_def"; |
|
47 val injection_defined_rev = thm "injection_defined_rev"; |
|
48 val injection_defined = thm "injection_defined"; |
|
49 val injection_eq = thm "injection_eq"; |
|
50 val injection_less = thm "injection_less"; |
|
51 val inst_cfun_pcpo = thm "inst_cfun_pcpo"; |
48 val Istrictify1 = thm "Istrictify1"; |
52 val Istrictify1 = thm "Istrictify1"; |
49 val Istrictify2 = thm "Istrictify2"; |
53 val Istrictify2 = thm "Istrictify2"; |
|
54 val Istrictify_def = thm "Istrictify_def"; |
|
55 val less_cfun_def = thm "less_CFun_def"; |
|
56 val less_cfun_ext = thm "less_cfun_ext"; |
|
57 val lub_cfun_mono = thm "lub_cfun_mono"; |
|
58 val lub_cfun = thm "lub_cfun"; |
|
59 val monofun_cfun_arg = thm "monofun_cfun_arg"; |
|
60 val monofun_cfun_fun = thm "monofun_cfun_fun"; |
|
61 val monofun_cfun = thm "monofun_cfun"; |
50 val monofun_Istrictify2 = thm "monofun_Istrictify2"; |
62 val monofun_Istrictify2 = thm "monofun_Istrictify2"; |
51 val contlub_Istrictify2 = thm "contlub_Istrictify2"; |
63 val monofun_Rep_CFun1 = thm "monofun_Rep_CFun1"; |
52 val cont_Istrictify1 = thm "cont_Istrictify1"; |
64 val monofun_Rep_CFun2 = thm "monofun_Rep_CFun2"; |
53 val cont_Istrictify2 = thm "cont_Istrictify2"; |
65 val oo_def = thm "oo_def"; |
|
66 val Rep_CFun_strict1 = thm "Rep_CFun_strict1"; |
|
67 val retraction_strict = thm "retraction_strict"; |
|
68 val semi_monofun_Abs_CFun = thm "semi_monofun_Abs_CFun"; |
54 val strictify1 = thm "strictify1"; |
69 val strictify1 = thm "strictify1"; |
55 val strictify2 = thm "strictify2"; |
70 val strictify2 = thm "strictify2"; |
56 val Rep_CFun_strict1 = thm "Rep_CFun_strict1"; |
71 val strictify_conv_if = thm "strictify_conv_if"; |
57 val chfin_Rep_CFunR = thm "chfin_Rep_CFunR"; |
72 val strictify_def = thm "strictify_def"; |
58 val retraction_strict = thm "retraction_strict"; |
73 val strictI = thm "strictI"; |
59 val injection_eq = thm "injection_eq"; |
74 val thelub_cfun = thm "thelub_cfun"; |
60 val injection_less = thm "injection_less"; |
75 val UU_CFun = thm "UU_CFun"; |
61 val injection_defined_rev = thm "injection_defined_rev"; |
|
62 val injection_defined = thm "injection_defined"; |
|
63 val chfin2chfin = thm "chfin2chfin"; |
|
64 val flat2flat = thm "flat2flat"; |
|
65 val flat_codom = thm "flat_codom"; |
|
66 val ID1 = thm "ID1"; |
|
67 val cfcomp1 = thm "cfcomp1"; |
|
68 val cfcomp2 = thm "cfcomp2"; |
|
69 val ID2 = thm "ID2"; |
|
70 val ID3 = thm "ID3"; |
|
71 val assoc_oo = thm "assoc_oo"; |
|
72 |
76 |
73 structure Cfun = |
77 structure Cfun = |
74 struct |
78 struct |
75 val thy = the_context (); |
79 val thy = the_context (); |
76 val Istrictify_def = Istrictify_def; |
80 val Istrictify_def = Istrictify_def; |