src/HOL/Nominal/nominal_atoms.ML
2009-06-23 haftmann 2009-06-23 add_datatype interface yields type names and less rules
2009-06-21 haftmann 2009-06-21 simplified names of common datatype types
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-17 haftmann 2009-06-17 datatype packages: record datatype_config for configuration flags; less verbose signatures
2009-05-07 haftmann 2009-05-07 explicit type_name antiquotations
2009-03-19 wenzelm 2009-03-19 proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in packages;
2009-03-04 nipkow 2009-03-04 Made Option a separate theory and renamed option_map to Option.map
2009-02-25 berghofe 2009-02-25 Added equivariance lemmas for fresh_star.
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2008-12-16 Christian Urban 2008-12-16 changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-11-10 berghofe 2008-11-10 Some more functions for accessing information about atoms.
2008-09-26 berghofe 2008-09-26 Added some more theorems to NominalData.
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-08-27 urbanc 2008-08-27 added equivariance lemmas for ex1 and the
2008-07-29 haftmann 2008-07-29 PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-06-30 urbanc 2008-06-30 added facts to lemma swap_simps and tuned lemma calc_atms
2008-06-14 wenzelm 2008-06-14 InductTacs.case_tac: removed obsolete declare, which is now part of Goal.prove;
2008-06-10 wenzelm 2008-06-10 InductTacs.case_tac with proper context and proper declaration of local variable;
2008-06-10 haftmann 2008-06-10 polished interface of datatype package
2008-06-09 wenzelm 2008-06-09 adapted case_tac/induct_tac;
2008-05-07 berghofe 2008-05-07 - Deleted arity proofs for set - Produce specific instances of theorems insert_eqvt, set_eqvt and perm_set_eq
2008-05-02 urbanc 2008-05-02 added more infrastructure for fresh_star
2008-03-29 wenzelm 2008-03-29 eliminated non-linear access to thy1 and thy12c;
2008-03-25 wenzelm 2008-03-25 removed redundant axiomatizations of XXX_infinite (fact already proven);
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;
2008-03-19 wenzelm 2008-03-19 auxiliary dynamic_thm(s) for fact lookup;
2008-02-18 urbanc 2008-02-18 added eqvt-flag to subseteq-lemma
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2007-12-06 haftmann 2007-12-06 added new primrec package
2007-12-05 haftmann 2007-12-05 map_product and fold_product
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-09-23 urbanc 2007-09-23 changed the representation of atoms to datatypes over nats
2007-09-13 berghofe 2007-09-13 Added equivariance lemmas for induct_forall.
2007-09-05 urbanc 2007-09-05 modified proofs so that they are not using claset()
2007-08-10 haftmann 2007-08-10 ClassPackage renamed to Class
2007-08-09 haftmann 2007-08-09 re-eliminated Option.thy
2007-08-07 haftmann 2007-08-07 split off theory Option for benefit of code generator
2007-07-21 wenzelm 2007-07-21 tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
2007-05-31 urbanc 2007-05-31 introduced symmetric variants of the lemmas for alpha-equivalence
2007-05-19 haftmann 2007-05-19 constant op @ now named append
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
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)