src/HOL/Nominal/Nominal.thy
2015-04-06 wenzelm 2015-04-06 local setup of induction tools, with restricted access to auxiliary consts; proper antiquotations for formerly inaccessible consts;
2014-09-18 blanchet 2014-09-18 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer) * * * made example compile again
2014-09-11 blanchet 2014-09-11 fixed some spelling mistakes
2014-09-11 blanchet 2014-09-11 updated news
2014-09-08 blanchet 2014-09-08 ported old Nominal to use new datatypes
2014-03-20 wenzelm 2014-03-20 more standard method_setup; enforce subgoal boundaries via SUBGOAL -- clean tactical failure if out-of-range;
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-03-15 wenzelm 2012-03-15 declare minor keywords via theory header;
2012-01-10 berghofe 2012-01-10 Reverted several lemmas involving sets to the state before the removal of the set type.
2011-12-24 haftmann 2011-12-24 treatment of type constructor `set`
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-11-24 wenzelm 2011-11-24 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-09-08 haftmann 2011-09-08 merged
2011-09-06 haftmann 2011-09-06 merged
2011-09-05 haftmann 2011-09-05 tuned
2011-09-04 haftmann 2011-09-04 pseudo-definition for perms on sets; tuned
2011-09-03 haftmann 2011-09-03 tuned specifications
2011-09-03 haftmann 2011-09-03 tuned specifications and proofs
2011-08-28 haftmann 2011-08-28 tuned
2011-02-21 wenzelm 2011-02-21 modernized specifications;
2011-01-15 berghofe 2011-01-15 Finally removed old primrec package, since Primrec.add_primrec_global can be used instead.
2011-01-14 wenzelm 2011-01-14 eliminated global prems; tuned proofs;
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-09-29 haftmann 2010-09-29 moved old_primrec source to nominal package, where it is still used
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-03-01 haftmann 2010-03-01 merged
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-24 wenzelm 2010-02-24 proper type syntax (cf. 7425aece4ee3);
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-21 Christian Urban 2009-09-21 tuned some proofs
2009-07-03 haftmann 2009-07-03 nominal.ML is nominal_datatype.ML
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-04-26 Christian Urban 2009-04-26 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
2009-04-25 Christian Urban 2009-04-25 adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-26 berghofe 2009-02-26 Added postprocessing rules for fresh_star.
2009-02-25 berghofe 2009-02-25 Added lemmas for normalizing freshness results involving fresh_star.
2009-02-25 berghofe 2009-02-25 Added equivariance lemmas for fresh_star.
2009-02-14 nipkow 2009-02-14 more finiteness changes
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-10-21 berghofe 2008-10-21 Added nominal_inductive2.ML
2008-09-26 berghofe 2008-09-26 Added some more lemmas that are useful in proof of strong induction rule.
2008-09-22 urbanc 2008-09-22 made the perm_simp tactic to understand options such as (no_asm)
2008-08-27 urbanc 2008-08-27 added equivariance lemmas for ex1 and the
2008-07-27 urbanc 2008-07-27 simplified a proof
2008-06-27 urbanc 2008-06-27 added a lemma to at_swap_simps
2008-06-16 wenzelm 2008-06-16 allE_Nil: only one copy, proven in regular theory source;
2008-05-08 urbanc 2008-05-08 added at_set_avoiding lemmas
2008-05-07 berghofe 2008-05-07 Adapted to encoding of sets as predicates
2008-05-02 urbanc 2008-05-02 added more infrastructure for fresh_star
2008-05-02 urbanc 2008-05-02 polished the proof for atm_prm_fresh and more lemmas for fresh_star
2008-04-03 urbanc 2008-04-03 added generalised definitions for freshness of sets of atoms and lists of atoms
2008-03-19 wenzelm 2008-03-19 more antiquotations;