1 |
1 |
2 (* legacy ML bindings *) |
2 (* legacy ML bindings *) |
3 |
3 |
4 val less_fun_def = thm "less_fun_def"; |
|
5 val refl_less_fun = thm "refl_less_fun"; |
|
6 val antisym_less_fun = thm "antisym_less_fun"; |
4 val antisym_less_fun = thm "antisym_less_fun"; |
7 val trans_less_fun = thm "trans_less_fun"; |
5 val app_strict = thm "app_strict"; |
8 val minimal_fun = thm "minimal_fun"; |
|
9 val least_fun = thm "least_fun"; |
|
10 val less_fun = thm "less_fun"; |
|
11 val ch2ch_fun = thm "ch2ch_fun"; |
6 val ch2ch_fun = thm "ch2ch_fun"; |
12 val ub2ub_fun = thm "ub2ub_fun"; |
7 val ch2ch_fun_rev = thm "ch2ch_fun_rev"; |
13 val lub_fun = thm "lub_fun"; |
|
14 val thelub_fun = thm "thelub_fun"; |
|
15 val cpo_fun = thm "cpo_fun"; |
8 val cpo_fun = thm "cpo_fun"; |
16 val inst_fun_pcpo = thm "inst_fun_pcpo"; |
9 val inst_fun_pcpo = thm "inst_fun_pcpo"; |
|
10 val least_fun = thm "least_fun"; |
|
11 val less_fun_def = thm "less_fun_def"; |
|
12 val less_fun_ext = thm "less_fun_ext"; |
|
13 val less_fun = thm "less_fun"; |
|
14 val lub_fun = thm "lub_fun"; |
|
15 val minimal_fun = thm "minimal_fun"; |
|
16 val refl_less_fun = thm "refl_less_fun"; |
|
17 val thelub_fun = thm "thelub_fun"; |
|
18 val trans_less_fun = thm "trans_less_fun"; |
|
19 val ub2ub_fun = thm "ub2ub_fun"; |
|
20 |