src/HOL/Nominal/Examples/Class.thy
2008-06-10 wenzelm 2008-06-10 case_split_tac (works without context);
2008-05-22 urbanc 2008-05-22 made the naming of the induction principles consistent: weak_induct is induct and induct is strong_induct
2008-05-17 wenzelm 2008-05-17 avoid undeclared variables within proofs;
2008-05-07 berghofe 2008-05-07 Adapted to encoding of sets as predicates
2008-04-14 wenzelm 2008-04-14 removed duplicate lemmas;
2008-02-18 urbanc 2008-02-18 updated
2007-07-11 berghofe 2007-07-11 - Renamed inductive2 to inductive - Renamed some theorems about transitive closure for predicates
2007-06-21 wenzelm 2007-06-21 tuned proofs -- avoid implicit prems;
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2007-05-31 urbanc 2007-05-31 introduced symmetric variants of the lemmas for alpha-equivalence
2007-05-25 urbanc 2007-05-25 adapted to fix for fresh_fun_simp
2007-05-24 urbanc 2007-05-24 temporary fix for a bug in fresh_fun_simp
2007-05-24 urbanc 2007-05-24 formalisation of my PhD (the result was correct, but the proof needed several corrections)
2007-03-28 berghofe 2007-03-28 - Renamed <predicate>_eqvt to <predicate>.eqvt - Renamed induct_weak to weak_induct
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-03 urbanc 2007-02-03 added the two renaming functions from my PhD
2006-04-28 berghofe 2006-04-28 Removed broken proof.
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-24 urbanc 2006-03-24 changed the it_prm proof to work for recursion
2006-03-22 urbanc 2006-03-22 added the first two simple proofs of the recursion combinator
2006-02-01 urbanc 2006-02-01 added all constructors from PhD
2006-01-11 urbanc 2006-01-11 updated to new induction principle
2005-12-16 urbanc 2005-12-16 I think the earlier version was completely broken (not sure about this one)
2005-12-13 urbanc 2005-12-13 initial commit (not to be seen by the public)