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.