src/HOL/Nominal/Nominal.thy
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;
2008-02-18 urbanc 2008-02-18 added eqvt-flag to subseteq-lemma
2008-01-24 berghofe 2008-01-24 Added lemma at_fin_set_fresh.
2007-09-14 urbanc 2007-09-14 reverted back to the old version of the equivariance lemma for ALL
2007-09-13 urbanc 2007-09-13 some cleaning up to do with contexts
2007-09-13 berghofe 2007-09-13 Added equivariance lemma for induct_implies.
2007-09-06 urbanc 2007-09-06 trivial cleaning up
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)