equal
deleted
inserted
replaced
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 declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt] |
|
656 |
|
657 equivariance alpha_tkind_raw |
655 equivariance alpha_tkind_raw |
658 |
656 |
659 thm eqvts |
657 thm eqvts |
660 thm eqvts_raw |
658 thm eqvts_raw |
661 |
659 |