changeset 18012 | 23e6cfda8c4b |
parent 17871 | 67ffbfcd6fef |
child 18047 | 3d643b13eb65 |
--- a/src/HOL/Nominal/Nominal.thy Fri Oct 28 16:35:40 2005 +0200 +++ b/src/HOL/Nominal/Nominal.thy Fri Oct 28 16:43:46 2005 +0200 @@ -2288,6 +2288,7 @@ (*******************************) (* permutation equality tactic *) use "nominal_permeq.ML"; + method_setup perm_simp = {* perm_eq_meth *} {* tactic for deciding equalities involving permutations *}