| changeset 2120 | 2786ff1df475 |
| parent 2105 | e25b0fff0dd2 |
| child 2142 | c39d4fe31100 |
| 2119:238062c4c9f2 | 2120:2786ff1df475 |
|---|---|
650 (*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} *) |
650 (*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} *) |
651 |
651 |
652 thm eqvts |
652 thm eqvts |
653 thm eqvts_raw |
653 thm eqvts_raw |
654 |
654 |
655 equivariance alpha_tkind_raw |
|
656 |
|
657 thm eqvts |
|
658 thm eqvts_raw |
|
659 |
655 |
660 end |
656 end |
661 |
657 |