1 |
1 |
2 (* legacy ML bindings *) |
2 (* legacy ML bindings *) |
3 |
3 |
4 val iterate_0 = thm "iterate_0"; |
4 val adm_chfindom = thm "adm_chfindom"; |
5 val iterate_Suc = thm "iterate_Suc"; |
5 val adm_impl_admw = thm "adm_impl_admw"; |
6 val Ifix_def = thm "Ifix_def"; |
|
7 val fix_def = thm "fix_def"; |
|
8 val admw_def = thm "admw_def"; |
6 val admw_def = thm "admw_def"; |
9 val iterate_Suc2 = thm "iterate_Suc2"; |
|
10 val chain_iterate2 = thm "chain_iterate2"; |
7 val chain_iterate2 = thm "chain_iterate2"; |
11 val chain_iterate = thm "chain_iterate"; |
8 val chain_iterate = thm "chain_iterate"; |
12 val Ifix_eq = thm "Ifix_eq"; |
9 val cont_Ifix = thm "cont_Ifix"; |
13 val Ifix_least = thm "Ifix_least"; |
|
14 val cont_iterate1 = thm "cont_iterate1"; |
10 val cont_iterate1 = thm "cont_iterate1"; |
15 val cont_iterate2 = thm "cont_iterate2"; |
11 val cont_iterate2 = thm "cont_iterate2"; |
16 val monofun_iterate2 = thm "monofun_iterate2"; |
12 val cont_iterate = thm "cont_iterate"; |
17 val contlub_iterate2 = thm "contlub_iterate2"; |
13 val contlub_iterate2 = thm "contlub_iterate2"; |
18 val cont_iterate = thm "cont_iterate"; |
14 val def_fix_ind = thm "def_fix_ind"; |
19 val cont_Ifix = thm "cont_Ifix"; |
15 val def_wfix_ind = thm "def_wfix_ind"; |
20 val fix_eq = thm "fix_eq"; |
16 val fix_const = thm "fix_const"; |
21 val fix_least = thm "fix_least"; |
17 val fix_def2 = thm "fix_def2"; |
22 val fix_eqI = thm "fix_eqI"; |
18 val fix_defined = thm "fix_defined"; |
|
19 val fix_defined_iff = thm "fix_defined_iff"; |
|
20 val fix_def = thm "fix_def"; |
23 val fix_eq2 = thm "fix_eq2"; |
21 val fix_eq2 = thm "fix_eq2"; |
24 val fix_eq3 = thm "fix_eq3"; |
22 val fix_eq3 = thm "fix_eq3"; |
25 val fix_eq4 = thm "fix_eq4"; |
23 val fix_eq4 = thm "fix_eq4"; |
26 val fix_eq5 = thm "fix_eq5"; |
24 val fix_eq5 = thm "fix_eq5"; |
27 val fix_def2 = thm "fix_def2"; |
25 val fix_eqI = thm "fix_eqI"; |
28 val def_fix_ind = thm "def_fix_ind"; |
26 val fix_eq = thm "fix_eq"; |
29 val adm_impl_admw = thm "adm_impl_admw"; |
27 val fix_id = thm "fix_id"; |
30 val fix_ind = thm "fix_ind"; |
28 val fix_ind = thm "fix_ind"; |
31 val def_fix_ind = thm "def_fix_ind"; |
29 val fix_least = thm "fix_least"; |
|
30 val fix_strict = thm "fix_strict"; |
|
31 val Ifix_def = thm "Ifix_def"; |
|
32 val Ifix_eq = thm "Ifix_eq"; |
|
33 val Ifix_least = thm "Ifix_least"; |
|
34 val iterate_0 = thm "iterate_0"; |
|
35 val iterate_Suc2 = thm "iterate_Suc2"; |
|
36 val iterate_Suc = thm "iterate_Suc"; |
|
37 val monofun_iterate2 = thm "monofun_iterate2"; |
32 val wfix_ind = thm "wfix_ind"; |
38 val wfix_ind = thm "wfix_ind"; |
33 val def_wfix_ind = thm "def_wfix_ind"; |
|
34 |
39 |
35 structure Fix = |
40 structure Fix = |
36 struct |
41 struct |
37 val thy = the_context (); |
42 val thy = the_context (); |
38 val Ifix_def = Ifix_def; |
43 val Ifix_def = Ifix_def; |