src/HOL/Nominal/Nominal.thy
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2007-05-31 urbanc 2007-05-31 tuned the proof
2007-05-31 urbanc 2007-05-31 introduced symmetric variants of the lemmas for alpha-equivalence
2007-05-20 urbanc 2007-05-20 added lemma for permutations on strings
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-05-03 urbanc 2007-05-03 tuned some of the proofs and added the lemma fresh_bool
2007-05-02 urbanc 2007-05-02 tuned some proofs and changed variable names in some definitions of Nominal.thy
2007-04-26 wenzelm 2007-04-26 eliminated unnamed infixes, tuned syntax;
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-24 narboux 2007-04-24 oups : wrong commit
2007-04-24 narboux 2007-04-24 adds op in front of an infix to fix SML compilation
2007-04-23 urbanc 2007-04-23 simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)
2007-04-21 urbanc 2007-04-21 tuned the setup of fresh_fun
2007-04-20 urbanc 2007-04-20 declared lemmas true_eqvt and false_eqvt to be equivariant (suggested by samth at ccs.neu.edu)
2007-04-19 narboux 2007-04-19 add a tactic to generate fresh names
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-16 urbanc 2007-04-16 added a more usuable lemma for dealing with fresh_fun
2007-04-12 urbanc 2007-04-12 tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
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-03 narboux 2007-04-03 remove the lemma swap_fun which was not needed
2007-03-27 urbanc 2007-03-27 added extended the lemma for equivariance of freshness
2007-03-25 urbanc 2007-03-25 moving lemmas into appropriate sections
2007-03-23 urbanc 2007-03-23 added the permutation operation on options to the list of equivariance lemmas
2007-03-22 urbanc 2007-03-22 corrected the lemmas min_nat_eqvt and min_int_eqvt
2007-03-16 urbanc 2007-03-16 added eqvt-lemmas for integers and eqvt-tagged the lemma append_eqvt
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-15 narboux 2007-02-15 start adding the attribute eqvt to some lemmas of the nominal library
2007-02-13 berghofe 2007-02-13 Added new file nominal_inductive.ML
2007-02-06 urbanc 2007-02-06 moved the infrastructure from the nominal_tags file to nominal_thmdecls file, and adapted the code to conform with informal Isabelle programming conventions
2007-02-02 urbanc 2007-02-02 added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
2006-11-27 berghofe 2006-11-27 Implemented new "nominal_primrec" command for defining functions on nominal datatypes.
2006-11-17 urbanc 2006-11-17 added an intro lemma for freshness of products; set up the simplifier so that it can deal with the compact and long notation for freshness constraints (FIXME: it should also be able to deal with the special case of freshness of atoms)
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-13 wenzelm 2006-11-13 added fresh_prodD, which is included fresh_prodD into mksimps setup;
2006-10-13 urbanc 2006-10-13 added the missing freshness-lemmas for nat, int, char and string and also the lemma for permutation acting on if's
2006-10-01 wenzelm 2006-10-01 moved theory Infinite_Set to Library;
2006-08-16 urbanc 2006-08-16 added missing supp_nat lemma
2006-07-04 berghofe 2006-07-04 - nominal_permeq.ML is now loaded before nominal_package.ML - methods and tactics in nominal_permeq.ML are now defined inside structure NominalPermeq, therefore the names in the method_setup section had to be changed
2006-07-02 urbanc 2006-07-02 added more infrastructure for the recursion combinator
2006-06-13 paulson 2006-06-13 removal of the obsolete "infinite_nonempty"
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 Removed comments around declaration of fresh_guess method.
2006-06-09 berghofe 2006-06-09 unique_names no longer set to false (thanks to improved naming scheme for "internal" constructors).
2006-06-05 urbanc 2006-06-05 added some further lemmas that deal with permutations and set-operators
2006-06-05 urbanc 2006-06-05 added the lemma perm_diff
2006-06-01 urbanc 2006-06-01 added the hack "reset NameSpace.unique_names" to Nominal.thy (Stefan is working on a real fix in the nominal_package)
2006-05-20 wenzelm 2006-05-20 primrec (unchecked);
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 defs (unchecked overloaded), including former primrec; tuned;
2006-05-05 urbanc 2006-05-05 added the lemma pt_fresh_bij2
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-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-03-26 urbanc 2006-03-26 simplified the proof at_fin_set_supp
2006-03-24 urbanc 2006-03-24 tuned some proofs
2006-03-08 urbanc 2006-03-08 tuned some of the proofs about fresh_fun
2006-03-01 urbanc 2006-03-01 added initialisation-code for finite_guess