src/HOL/Nominal/nominal_atoms.ML
2007-05-07 ago simplified DataFun interfaces;
2007-04-25 ago add the lemma supp_eqvt and put the right attribute
2007-04-24 ago fixes last commit
2007-04-24 ago add two lemmas dealing with freshness on permutations.
2007-04-23 ago simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)
2007-04-20 ago moved axclass module closer to core system
2007-04-16 ago 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 ago deleted remaining instances of swap_simp_a and swap_simp_b (obsolete now)
2007-04-07 ago tuned slightly the previous commit
2007-04-07 ago perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a
2007-03-31 ago added pt_bij' to the collection perm_swap and also added abs_perm to the collection of equivariance lemmas
2007-03-28 ago made the type sets instance of the "cp" type-class
2007-03-27 ago added extended the lemma for equivariance of freshness
2007-03-06 ago major update of the nominal package; there is now an infrastructure
2007-02-07 ago Adapted to changes in Finite_Set theory.
2006-12-06 ago removed legacy ML bindings;
2006-11-15 ago replaced exists_fresh lemma with a version formulated with obtains;
2006-11-10 ago deleted all uses of sign_of as it's now the identity function
2006-08-14 ago Removed non-trivial definitions from calc_atm theorem list.
2006-07-21 ago adaption to argument change in primrec_package
2006-07-11 ago replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
2006-07-08 ago Goal.prove_global;
2006-07-04 ago added simplification rules to the fresh_guess tactic
2006-07-04 ago made calc_atm stronger by including some relative
2006-07-02 ago added more infrastructure for the recursion combinator
2006-05-15 ago added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
2006-05-13 ago unchecked definitions;
2006-05-05 ago added the lemma abs_fun_eq' to the nominal theory,
2006-05-03 ago added lemma fresh_right, which is useful
2006-04-30 ago AxClass.define_class_i;
2006-04-28 ago Renamed "nominal" theory to "Nominal".
2006-04-27 ago Adapted to new interface of add_axclass_i.
2006-04-27 ago isar-keywords.el
2006-03-15 ago add_inst_arity_i renamed to prove_arity.
2006-03-01 ago added fresh_fun_eqvt theorem to the theorem collection
2006-02-26 ago improved the decision-procedure for permutations;
2006-02-24 ago Reverted to old interface of AxClass.add_inst_arity(_i)
2006-02-24 ago Adapted to Florian's recent changes to the AxClass package.
2006-01-23 ago Updated to Isabelle 2006-01-23
2006-01-22 ago made the change for setup-functions not returning functions
2006-01-19 ago Use generic Simplifier.simp_add attribute instead
2006-01-11 ago rolled back the last addition since these lemmas were already
2006-01-11 ago added the thms-collection "pt_id" (collection of all pt_<ak>1 lemmas)
2006-01-09 ago added some lemmas to the collection "abs_fresh"
2006-01-07 ago added private datatype nprod (copy of prod) to be
2006-01-05 ago changed the name of the type "nOption" to "noption".
2005-12-19 ago made the changes according to Florian's re-arranging of
2005-12-19 ago added proofs to show that every atom-kind combination
2005-12-19 ago added thms to perm_compose (so far only composition
2005-12-19 ago tuned one comment
2005-12-18 ago more cleaning up - this time of the cp-instance
2005-12-18 ago improved the finite-support proof
2005-12-18 ago improved the code for showing that a type is
2005-12-16 ago added container-lemma fresh_eqvt
2005-12-13 ago added a fresh_left lemma that contains all instantiation
2005-12-10 ago changed the types in accordance with Florian's changes
2005-12-08 ago Adapted to new type of PureThy.add_defs_i.
2005-12-05 ago added code to say that discrete types (nat, bool, char)
2005-11-30 ago added facilities to prove the pt and fs instances
2005-11-29 ago made some of the theorem look-ups static (by using