equal
deleted
inserted
replaced
25 thm trm_assg.inducts |
25 thm trm_assg.inducts |
26 thm trm_assg.distinct |
26 thm trm_assg.distinct |
27 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} |
27 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} |
28 thm trm_assg.fv[simplified trm_assg.supp(1-2)] |
28 thm trm_assg.fv[simplified trm_assg.supp(1-2)] |
29 |
29 |
30 (* |
|
31 setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} |
|
32 declare permute_trm_raw_permute_assg_raw.simps[eqvt] |
30 declare permute_trm_raw_permute_assg_raw.simps[eqvt] |
33 declare alpha_gen_eqvt[eqvt] |
31 declare alpha_gen_eqvt[eqvt] |
|
32 |
34 equivariance alpha_trm_raw |
33 equivariance alpha_trm_raw |
35 *) |
34 |
36 |
35 |
37 end |
36 end |
38 |
37 |
39 |
38 |
40 |
39 |