src/HOL/Nominal/nominal_atoms.ML
2007-04-25 narboux 2007-04-25 add the lemma supp_eqvt and put the right attribute
2007-04-24 narboux 2007-04-24 fixes last commit
2007-04-24 narboux 2007-04-24 add two lemmas dealing with freshness on permutations.
2007-04-23 urbanc 2007-04-23 simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)
2007-04-20 haftmann 2007-04-20 moved axclass module closer to core system
2007-04-16 urbanc 2007-04-16 improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
2007-04-07 urbanc 2007-04-07 deleted remaining instances of swap_simp_a and swap_simp_b (obsolete now)
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-03-31 urbanc 2007-03-31 added pt_bij' to the collection perm_swap and also added abs_perm to the collection of equivariance lemmas
2007-03-28 urbanc 2007-03-28 made the type sets instance of the "cp" type-class
2007-03-27 urbanc 2007-03-27 added extended the lemma for equivariance of freshness
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-15 urbanc 2006-11-15 replaced exists_fresh lemma with a version formulated with obtains; old lemma is available as exists_fresh' (still needed in apply-scripts)
2006-11-10 urbanc 2006-11-10 deleted all uses of sign_of as it's now the identity function
2006-08-14 berghofe 2006-08-14 Removed non-trivial definitions from calc_atm theorem list.
2006-07-21 haftmann 2006-07-21 adaption to argument change in primrec_package
2006-07-11 webertj 2006-07-11 replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
2006-07-08 wenzelm 2006-07-08 Goal.prove_global;
2006-07-04 urbanc 2006-07-04 added simplification rules to the fresh_guess tactic
2006-07-04 urbanc 2006-07-04 made calc_atm stronger by including some relative obvious simplification rules
2006-07-02 urbanc 2006-07-02 added more infrastructure for the recursion combinator
2006-05-15 urbanc 2006-05-15 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq (they are used in the proof of the strong induction principle) added code to nominal_atoms to collect these lemmas in "fresh_aux" instantiated for each atom type deleted the fresh_fun_eqvt from nominal_atoms, since fresh_fun is not used anymore in the recursion combinator
2006-05-13 wenzelm 2006-05-13 unchecked definitions;
2006-05-05 urbanc 2006-05-05 added the lemma abs_fun_eq' to the nominal theory, and also added code to nominal_atoms for generating the theorem-list alpha'
2006-05-03 urbanc 2006-05-03 added lemma fresh_right, which is useful in the proof of the recursion combinator
2006-04-30 wenzelm 2006-04-30 AxClass.define_class_i;
2006-04-28 berghofe 2006-04-28 Renamed "nominal" theory to "Nominal".
2006-04-27 berghofe 2006-04-27 Adapted to new interface of add_axclass_i.
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-03-15 berghofe 2006-03-15 add_inst_arity_i renamed to prove_arity.
2006-03-01 urbanc 2006-03-01 added fresh_fun_eqvt theorem to the theorem collection
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
2006-02-24 berghofe 2006-02-24 Reverted to old interface of AxClass.add_inst_arity(_i)
2006-02-24 berghofe 2006-02-24 Adapted to Florian's recent changes to the AxClass package.
2006-01-23 krauss 2006-01-23 Updated to Isabelle 2006-01-23
2006-01-22 urbanc 2006-01-22 made the change for setup-functions not returning functions anymore
2006-01-19 berghofe 2006-01-19 Use generic Simplifier.simp_add attribute instead of Simplifier.simp_add_global.
2006-01-11 urbanc 2006-01-11 rolled back the last addition since these lemmas were already in the simpset.
2006-01-11 urbanc 2006-01-11 added the thms-collection "pt_id" (collection of all pt_<ak>1 lemmas)
2006-01-09 urbanc 2006-01-09 added some lemmas to the collection "abs_fresh" the lemmas are of the form finite (supp x) ==> (b # [a].x) = (b=a \/ b # x) previously only lemmas of the form (b # [a].x) = (b=a \/ b # x) with the type-constraint that x is finitely supported were included.
2006-01-07 urbanc 2006-01-07 added private datatype nprod (copy of prod) to be used in the induction rule
2006-01-05 urbanc 2006-01-05 changed the name of the type "nOption" to "noption".
2005-12-19 urbanc 2005-12-19 made the changes according to Florian's re-arranging of tuples (everything up to 19th December).
2005-12-19 urbanc 2005-12-19 added proofs to show that every atom-kind combination is in the respective finite-support class (now have to adjust the files according to Florian's changes)
2005-12-19 urbanc 2005-12-19 added thms to perm_compose (so far only composition theorems were included where the type of the permutation was equal)
2005-12-19 urbanc 2005-12-19 tuned one comment
2005-12-18 urbanc 2005-12-18 more cleaning up - this time of the cp-instance proofs
2005-12-18 urbanc 2005-12-18 improved the finite-support proof added finite support proof for options (I am surprised that one does not need more fs-proofs; at the moment only lists, products, units and atoms are shown to be finitely supported (of course also every nominal datatype is finitely supported)) deleted pt_bool_inst - not necessary because discrete types are treated separately in nominal_atoms
2005-12-18 urbanc 2005-12-18 improved the code for showing that a type is in the pt-axclass (I try to slowly overcome my incompetence with such ML-code).
2005-12-16 urbanc 2005-12-16 added container-lemma fresh_eqvt (definition: container-lemma contains all instantiations of a lemma from the general theory)
2005-12-13 urbanc 2005-12-13 added a fresh_left lemma that contains all instantiation for the various atom-types.
2005-12-10 urbanc 2005-12-10 changed the types in accordance with Florian's changes
2005-12-08 berghofe 2005-12-08 Adapted to new type of PureThy.add_defs_i.
2005-12-05 urbanc 2005-12-05 added code to say that discrete types (nat, bool, char) are instances of cp_*_*.
2005-11-30 urbanc 2005-11-30 added facilities to prove the pt and fs instances for discrete types
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-27 urbanc 2005-11-27 finished cleaning up the parts that collect lemmas (with instantiations) under some general names