|
3655
|
1 |
|
|
12026
|
2 |
(* legacy ML bindings *)
|
|
3324
|
3 |
|
|
12026
|
4 |
structure lift =
|
|
|
5 |
struct
|
|
|
6 |
val distinct = thms "lift.distinct";
|
|
|
7 |
val inject = thms "lift.inject";
|
|
|
8 |
val exhaust = thm "lift.exhaust";
|
|
|
9 |
val cases = thms "lift.cases";
|
|
|
10 |
val split = thm "lift.split";
|
|
|
11 |
val split_asm = thm "lift.split_asm";
|
|
|
12 |
val induct = thm "lift.induct";
|
|
|
13 |
val recs = thms "lift.recs";
|
|
|
14 |
val simps = thms "lift.simps";
|
|
|
15 |
val size = thms "lift.size";
|
|
|
16 |
end;
|
|
3324
|
17 |
|
|
12026
|
18 |
val Def_not_UU = thm "Def_not_UU";
|
|
|
19 |
val DefE = thm "DefE";
|
|
|
20 |
val DefE2 = thm "DefE2";
|
|
|
21 |
val Def_inject_less_eq = thm "Def_inject_less_eq";
|
|
|
22 |
val Def_less_is_eq = thm "Def_less_is_eq";
|
|
|
23 |
val Lift_cases = thm "Lift_cases";
|
|
|
24 |
val Lift_exhaust = thm "Lift_exhaust";
|
|
|
25 |
val UU_lift_def = thm "UU_lift_def";
|
|
|
26 |
val Undef_eq_UU = thm "Undef_eq_UU";
|
|
|
27 |
val cont2cont_CF1L_rev2 = thm "cont2cont_CF1L_rev2";
|
|
|
28 |
val cont_Rep_CFun_app = thm "cont_Rep_CFun_app";
|
|
|
29 |
val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app";
|
|
|
30 |
val cont_flift1_arg = thm "cont_flift1_arg";
|
|
|
31 |
val cont_flift1_arg_and_not_arg = thm "cont_flift1_arg_and_not_arg";
|
|
|
32 |
val cont_flift1_not_arg = thm "cont_flift1_not_arg";
|
|
|
33 |
val cont_flift2_arg = thm "cont_flift2_arg";
|
|
|
34 |
val cont_if = thm "cont_if";
|
|
|
35 |
val flat_imp_chfin_poo = thm "flat_imp_chfin_poo";
|
|
|
36 |
val flift1_Def = thm "flift1_Def";
|
|
|
37 |
val flift1_UU = thm "flift1_UU";
|
|
|
38 |
val flift1_def = thm "flift1_def";
|
|
|
39 |
val flift2_Def = thm "flift2_Def";
|
|
|
40 |
val flift2_UU = thm "flift2_UU";
|
|
|
41 |
val flift2_def = thm "flift2_def";
|
|
|
42 |
val flift2_nUU = thm "flift2_nUU";
|
|
|
43 |
val inst_lift_pcpo = thm "inst_lift_pcpo";
|
|
|
44 |
val inst_lift_po = thm "inst_lift_po";
|
|
|
45 |
val least_lift = thm "least_lift";
|
|
|
46 |
val less_lift = thm "less_lift";
|
|
|
47 |
val less_lift_def = thm "less_lift_def";
|
|
|
48 |
val liftpair_def = thm "liftpair_def";
|
|
|
49 |
val minimal_lift = thm "minimal_lift";
|
|
|
50 |
val not_Undef_is_Def = thm "not_Undef_is_Def";
|