equal
deleted
inserted
replaced
23 |
23 |
24 (* can lift *) |
24 (* can lift *) |
25 |
25 |
26 thm distinct |
26 thm distinct |
27 thm trm_raw_assg_raw.inducts |
27 thm trm_raw_assg_raw.inducts |
|
28 thm trm_raw.exhaust |
|
29 thm assg_raw.exhaust |
28 thm fv_defs |
30 thm fv_defs |
29 thm perm_simps |
31 thm perm_simps |
30 thm perm_laws |
32 thm perm_laws |
31 thm trm_raw_assg_raw.size(9 - 16) |
33 thm trm_raw_assg_raw.size(9 - 16) |
32 thm eq_iff |
34 thm eq_iff |
35 thm fv_eqvt |
37 thm fv_eqvt |
36 thm bn_eqvt |
38 thm bn_eqvt |
37 thm size_eqvt |
39 thm size_eqvt |
38 |
40 |
39 |
41 |
40 (* eqvt lemmas for fv / fv_bn / bn *) |
|
41 |
|
42 ML {* |
42 ML {* |
43 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
43 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
44 *} |
44 *} |
45 |
45 |
46 ML {* |
46 ML {* |
47 val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.inducts} |
47 val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.inducts} |
|
48 *} |
|
49 |
|
50 ML {* |
|
51 val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw.exhaust} |
|
52 *} |
|
53 |
|
54 ML {* |
|
55 val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms assg_raw.exhaust} |
48 *} |
56 *} |
49 |
57 |
50 ML {* |
58 ML {* |
51 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs} |
59 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs} |
52 *} |
60 *} |