author | wenzelm |
Wed, 14 Sep 2005 22:04:34 +0200 | |
changeset 17383 | 3eb21fb8c2ec |
parent 16922 | 2128ac2aa5db |
permissions | -rw-r--r-- |
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 |
|
16922 | 18 |
val cont2cont_flift1 = thm "cont2cont_flift1"; |
19 |
val cont2cont_lift_case = thm "cont2cont_lift_case"; |
|
20 |
val cont_flift1 = thm "cont_flift1"; |
|
21 |
val cont_lemmas_ext = thms "cont_lemmas_ext"; |
|
22 |
val cont_lift_case1 = thm "cont_lift_case1"; |
|
23 |
val cont_lift_case2 = thm "cont_lift_case2"; |
|
24 |
val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app"; |
|
25 |
val cont_Rep_CFun_app = thm "cont_Rep_CFun_app"; |
|
26 |
val DefE2 = thm "DefE2"; |
|
12026 | 27 |
val DefE = thm "DefE"; |
28 |
val Def_inject_less_eq = thm "Def_inject_less_eq"; |
|
16922 | 29 |
val Def_inject = thm "Def_inject"; |
12026 | 30 |
val Def_less_is_eq = thm "Def_less_is_eq"; |
16922 | 31 |
val Def_not_UU = thm "Def_not_UU"; |
32 |
val flift1_def = thm "flift1_def"; |
|
12026 | 33 |
val flift1_Def = thm "flift1_Def"; |
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16388
diff
changeset
|
34 |
val flift1_strict = thm "flift1_strict"; |
16922 | 35 |
val flift2_defined = thm "flift2_defined"; |
36 |
val flift2_def = thm "flift2_def"; |
|
12026 | 37 |
val flift2_Def = thm "flift2_Def"; |
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16388
diff
changeset
|
38 |
val flift2_strict = thm "flift2_strict"; |
16922 | 39 |
val inst_lift_pcpo = thm "inst_lift_pcpo"; |
40 |
val less_lift_def = thm "less_lift_def"; |
|
12026 | 41 |
val less_lift = thm "less_lift"; |
16922 | 42 |
val Lift_cases = thm "Lift_cases"; |
43 |
val lift_definedE = thm "lift_definedE"; |
|
44 |
val lift_distinct1 = thm "lift_distinct1"; |
|
45 |
val lift_distinct2 = thm "lift_distinct2"; |
|
46 |
val Lift_exhaust = thm "Lift_exhaust"; |
|
47 |
val lift_induct = thm "lift_induct"; |
|
12026 | 48 |
val liftpair_def = thm "liftpair_def"; |
49 |
val not_Undef_is_Def = thm "not_Undef_is_Def"; |