src/HOL/Nominal/nominal_permeq.ML
2007-04-07 urbanc 2007-04-07 tuned slightly the previous commit
2007-04-07 narboux 2007-04-07 perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a
2007-04-04 narboux 2007-04-04 make fresh_guess fail if it does not solve the subgoal
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2007-04-03 narboux 2007-04-03 remove the lemma swap_fun which was not needed
2007-04-02 narboux 2007-04-02 rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
2007-03-28 urbanc 2007-03-28 the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
2007-03-06 urbanc 2007-03-06 major update of the nominal package; there is now an infrastructure for equivariance lemmas which eases definitions of nominal functions
2007-02-07 berghofe 2007-02-07 Adapted to changes in Finite_Set theory.
2006-12-06 wenzelm 2006-12-06 removed legacy ML bindings;
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-10-20 haftmann 2006-10-20 slight cleanup
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-08-29 urbanc 2006-08-29 added a FIXME-comment
2006-08-02 wenzelm 2006-08-02 normalized Proof.context/method type aliases;
2006-07-04 urbanc 2006-07-04 added simplification rules to the fresh_guess tactic
2006-07-04 berghofe 2006-07-04 - put declarations inside a structure (NominalPermeq) - dynamic_thm(s) now looks up theorems in theory associated with proof state (rather than in context associated with simpset) - finite_guess_tac now automatically adds some extra rules about supp to the simpset
2006-06-12 urbanc 2006-06-12 added lemma fresh_unit to Nominal.thy made the fresh_guess tactic to solve more goals adapted Iteration.thy to use the new tactic
2006-06-12 berghofe 2006-06-12 Added fresh_guess_tac.
2006-04-28 berghofe 2006-04-28 Renamed "nominal" theory to "Nominal".
2006-04-27 urbanc 2006-04-27 isar-keywords.el - I am not sure what has changed here nominal.thy - includes a number of new lemmas (including freshness and perm_aux things) nominal_atoms.ML - no particular changes here nominal_permeq.ML - a new version of the decision procedure using for permutation composition the constant perm_aux examples - various adjustments
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.