equal
deleted
inserted
replaced
741 unfolding unpermute_def by simp |
741 unfolding unpermute_def by simp |
742 |
742 |
743 text {* provides perm_simp methods *} |
743 text {* provides perm_simp methods *} |
744 |
744 |
745 use "nominal_permeq.ML" |
745 use "nominal_permeq.ML" |
746 setup Nominal_Permeq.setup |
|
747 |
746 |
748 method_setup perm_simp = |
747 method_setup perm_simp = |
749 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *} |
748 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *} |
750 {* pushes permutations inside. *} |
749 {* pushes permutations inside. *} |
751 |
750 |