src/HOL/Nominal/nominal_permeq.ML
2006-04-06 urbanc 2006-04-06 modified the perm_compose rule such that it is applied as simplification rule (as simproc) in the restricted case where the first permutation is a swapping coming from a supports problem also deleted the perm_compose' rule from the set of rules that are automatically tried
2006-03-01 urbanc 2006-03-01 fixed a problem where a permutation is not analysed when the term is of the form (pi o f) x1...xn This was the case because the head of this term is the constant "nominal.perm". Now an applicability predicate decides the right behaviour of the simproc
2006-03-01 urbanc 2006-03-01 made some small tunings in the decision-procedure (in the order how the "small" tactics are called)
2006-02-27 urbanc 2006-02-27 added a finite_guess tactic, which solves automatically finite-support goals
2006-02-27 urbanc 2006-02-27 added support for arbitrary atoms in the simproc
2006-02-26 urbanc 2006-02-26 improved the decision-procedure for permutations; now uses a simproc FIXME: the simproc still needs to be adapted for arbitrary atom types
2005-12-19 urbanc 2005-12-19 fixed a bug that occured when more than one atom-type is declared.
2005-11-29 urbanc 2005-11-29 made some of the theorem look-ups static (by using thm instead of PureThy.get_thm)
2005-11-01 urbanc 2005-11-01 tunings of some comments (nothing serious)
2005-10-29 urbanc 2005-10-29 Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'. This means the syntax of the tactics supports_simp and perm_simp are exactly like simp, namely (supports_simp add: .... del: ...) where the add's and del's are optional.
2005-10-28 urbanc 2005-10-28 Added (optional) arguments to the tactics perm_eq_simp and supports_simp. They now follow the "simp"-way and use the syntax: apply(supports_simp simp add: thms) etc.
2005-10-17 berghofe 2005-10-17 Initial revision.