| changeset 1277 | 6eacf60ce41d |
| parent 1274 | d867021d8ac1 |
| child 1278 | 8814494fe4da |
| 1276:3365fce80f0f | 1277:6eacf60ce41d |
|---|---|
25 where |
25 where |
26 "bv1 (BUnit) = {}" |
26 "bv1 (BUnit) = {}" |
27 | "bv1 (BVr x) = {atom x}" |
27 | "bv1 (BVr x) = {atom x}" |
28 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
28 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
29 |
29 |
30 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Term1.rtrm1", "Term1.bp"] *} |
30 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term1.rtrm1") 2 *} |
31 thm permute_rtrm1_permute_bp.simps |
31 thm permute_rtrm1_permute_bp.simps |
32 |
32 |
33 local_setup {* |
33 local_setup {* |
34 snd o define_fv_alpha "Term1.rtrm1" |
34 snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1") |
35 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
35 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
36 [[], [[]], [[], []]]] *} |
36 [[], [[]], [[], []]]] *} |
37 |
37 |
38 notation |
38 notation |
39 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
39 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |