|
1 |
|
2 (* legacy ML bindings *) |
|
3 |
|
4 val less_cfun_def = thm "less_cfun_def"; |
|
5 val Rep_Cfun = thm "Rep_Cfun"; |
|
6 val Rep_Cfun_inverse = thm "Rep_Cfun_inverse"; |
|
7 val Abs_Cfun_inverse = thm "Abs_Cfun_inverse"; |
|
8 val refl_less_cfun = thm "refl_less_cfun"; |
|
9 val antisym_less_cfun = thm "antisym_less_cfun"; |
|
10 val trans_less_cfun = thm "trans_less_cfun"; |
|
11 val cfun_cong = thm "cfun_cong"; |
|
12 val cfun_fun_cong = thm "cfun_fun_cong"; |
|
13 val cfun_arg_cong = thm "cfun_arg_cong"; |
|
14 val Abs_Cfun_inverse2 = thm "Abs_Cfun_inverse2"; |
|
15 val Cfunapp2 = thm "Cfunapp2"; |
|
16 val beta_cfun = thm "beta_cfun"; |
|
17 val inst_cfun_po = thm "inst_cfun_po"; |
|
18 val less_cfun = thm "less_cfun"; |
|
19 val minimal_cfun = thm "minimal_cfun"; |
|
20 val UU_cfun_def = thm "UU_cfun_def"; |
|
21 val least_cfun = thm "least_cfun"; |
|
22 val cont_Rep_CFun2 = thm "cont_Rep_CFun2"; |
|
23 val monofun_Rep_CFun2 = thm "monofun_Rep_CFun2"; |
|
24 val contlub_Rep_CFun2 = thm "contlub_Rep_CFun2"; |
|
25 val cont_cfun_arg = thm "cont_cfun_arg"; |
|
26 val contlub_cfun_arg = thm "contlub_cfun_arg"; |
|
27 val monofun_Rep_CFun1 = thm "monofun_Rep_CFun1"; |
|
28 val monofun_cfun_fun = thm "monofun_cfun_fun"; |
|
29 val monofun_cfun_arg = thm "monofun_cfun_arg"; |
|
30 val chain_monofun = thm "chain_monofun"; |
|
31 val monofun_cfun = thm "monofun_cfun"; |
|
32 val strictI = thm "strictI"; |
|
33 val ch2ch_Rep_CFunR = thm "ch2ch_Rep_CFunR"; |
|
34 val ch2ch_Rep_CFunL = thm "ch2ch_Rep_CFunL"; |
|
35 val lub_cfun_mono = thm "lub_cfun_mono"; |
|
36 val ex_lubcfun = thm "ex_lubcfun"; |
|
37 val cont_lubcfun = thm "cont_lubcfun"; |
|
38 val lub_cfun = thm "lub_cfun"; |
|
39 val thelub_cfun = thm "thelub_cfun"; |
|
40 val cpo_cfun = thm "cpo_cfun"; |
|
41 val ext_cfun = thm "ext_cfun"; |
|
42 val semi_monofun_Abs_CFun = thm "semi_monofun_Abs_CFun"; |
|
43 val less_cfun2 = thm "less_cfun2"; |
|
44 val Istrictify_def = thm "Istrictify_def"; |
|
45 val strictify_def = thm "strictify_def"; |
|
46 val ID_def = thm "ID_def"; |
|
47 val oo_def = thm "oo_def"; |
|
48 val inst_cfun_pcpo = thm "inst_cfun_pcpo"; |
|
49 val contlub_Rep_CFun1 = thm "contlub_Rep_CFun1"; |
|
50 val cont_Rep_CFun1 = thm "cont_Rep_CFun1"; |
|
51 val contlub_cfun_fun = thm "contlub_cfun_fun"; |
|
52 val cont_cfun_fun = thm "cont_cfun_fun"; |
|
53 val contlub_cfun = thm "contlub_cfun"; |
|
54 val cont_cfun = thm "cont_cfun"; |
|
55 val cont2cont_Rep_CFun = thm "cont2cont_Rep_CFun"; |
|
56 val cont2mono_LAM = thm "cont2mono_LAM"; |
|
57 val cont2cont_LAM = thm "cont2cont_LAM"; |
|
58 val cont_lemmas1 = [cont_const, cont_id, cont_Rep_CFun2, |
|
59 cont2cont_Rep_CFun, cont2cont_LAM]; |
|
60 val strict_Rep_CFun1 = thm "strict_Rep_CFun1"; |
|
61 val Istrictify1 = thm "Istrictify1"; |
|
62 val Istrictify2 = thm "Istrictify2"; |
|
63 val monofun_Istrictify1 = thm "monofun_Istrictify1"; |
|
64 val monofun_Istrictify2 = thm "monofun_Istrictify2"; |
|
65 val contlub_Istrictify1 = thm "contlub_Istrictify1"; |
|
66 val contlub_Istrictify2 = thm "contlub_Istrictify2"; |
|
67 val cont_Istrictify1 = thm "cont_Istrictify1"; |
|
68 val cont_Istrictify2 = thm "cont_Istrictify2"; |
|
69 val strictify1 = thm "strictify1"; |
|
70 val strictify2 = thm "strictify2"; |
|
71 val chfin_Rep_CFunR = thm "chfin_Rep_CFunR"; |
|
72 val iso_strict = thm "iso_strict"; |
|
73 val isorep_defined = thm "isorep_defined"; |
|
74 val isoabs_defined = thm "isoabs_defined"; |
|
75 val chfin2chfin = thm "chfin2chfin"; |
|
76 val flat2flat = thm "flat2flat"; |
|
77 val flat_codom = thm "flat_codom"; |
|
78 val ID1 = thm "ID1"; |
|
79 val cfcomp1 = thm "cfcomp1"; |
|
80 val cfcomp2 = thm "cfcomp2"; |
|
81 val ID2 = thm "ID2"; |
|
82 val ID3 = thm "ID3"; |
|
83 val assoc_oo = thm "assoc_oo"; |
|
84 |
|
85 structure Cfun = |
|
86 struct |
|
87 val thy = the_context (); |
|
88 val Istrictify_def = Istrictify_def; |
|
89 val strictify_def = strictify_def; |
|
90 val ID_def = ID_def; |
|
91 val oo_def = oo_def; |
|
92 end; |