src/HOL/Nominal/Examples/Fsub.thy
2012-11-28 wenzelm 2012-11-28 eliminated slightly odd identifiers;
2012-09-05 wenzelm 2012-09-05 tuned proofs;
2012-01-11 berghofe 2012-01-11 Removed strange hack introduced in b27e93132603, since equivariance is working again
2011-12-24 haftmann 2011-12-24 explicitly spelt out proof of equivariance avoids problem with automation due to type constructor `set`
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-02-21 wenzelm 2011-02-21 modernized specifications;
2010-09-08 haftmann 2010-09-08 modernized primrec
2010-03-02 haftmann 2010-03-02 repaired subscripts broken in d8d7d1b785af
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-01-10 berghofe 2010-01-10 Adapted to changes in induct method.
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-07-15 Christian Urban 2009-07-15 simplified proofs
2009-04-26 Christian Urban 2009-04-26 deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
2009-02-25 berghofe 2009-02-25 Added typing and evaluation relations, together with proofs of preservation and progress (i.e. part 2A of the POPLmark challenge).
2008-12-13 berghofe 2008-12-13 Modified nominal_primrec to make it work with local theories, unified syntax with the one used by fun(ction) and new version of primrec command.
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-02-18 urbanc 2008-02-18 updated
2007-07-11 berghofe 2007-07-11 Renamed inductive2 to inductive.
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2007-04-19 berghofe 2007-04-19 nominal_inductive no longer proves equivariance.
2007-03-28 berghofe 2007-03-28 - Renamed <predicate>_eqvt to <predicate>.eqvt - Renamed induct_weak to weak_induct
2007-03-28 urbanc 2007-03-28 the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
2007-03-28 urbanc 2007-03-28 adapted to nominal_inductive infrastructure
2007-03-12 berghofe 2007-03-12 Adapted to new inductive definition package.
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
2006-11-27 berghofe 2006-11-27 Adapted to new nominal_primrec command.
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)
2006-10-23 berghofe 2006-10-23 Adapted to changes in FCBs.
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
2006-08-18 urbanc 2006-08-18 adapted using the characteristic equations
2006-08-17 urbanc 2006-08-17 added definition for size and substitution using the recursion combinator
2006-07-02 urbanc 2006-07-02 added more infrastructure for the recursion combinator
2006-04-28 berghofe 2006-04-28 Capitalized theory names.
2006-01-22 urbanc 2006-01-22 no essential changes
2006-01-11 urbanc 2006-01-11 cahges to use the new induction-principle (now proved in full glory)
2006-01-11 urbanc 2006-01-11 merged the silly lemmas into the eqvt proof of subtype
2006-01-11 urbanc 2006-01-11 tuned
2006-01-10 urbanc 2006-01-10 tuned
2006-01-09 urbanc 2006-01-09 commented the transitivity and narrowing proof
2006-01-04 urbanc 2006-01-04 added more documentation; will now try out a modification of the ok-predicate
2005-12-16 urbanc 2005-12-16 tuned more proofs
2005-12-15 urbanc 2005-12-15 there was a small error in the last commit - fixed now
2005-12-15 urbanc 2005-12-15 tuned more proof and added in-file documentation
2005-12-15 urbanc 2005-12-15 tuned the proof of transitivity/narrowing
2005-12-15 urbanc 2005-12-15 made further tunings
2005-12-05 urbanc 2005-12-05 transitivity should be now in a reasonable state. But Markus has to have a look at some of the advanced features.
2005-11-30 urbanc 2005-11-30 started to change the transitivity/narrowing case: have trouble with Q=Q.
2005-11-30 urbanc 2005-11-30 changed everything until the interesting transitivity_narrowing proof.
2005-11-28 urbanc 2005-11-28 some small tuning
2005-11-27 urbanc 2005-11-27 added an authors section (please let me know if somebody is left out or unhappy)
2005-11-27 urbanc 2005-11-27 cleaned up all examples so that they work with the current nominal-setting.
2005-11-25 urbanc 2005-11-25 added fsub.thy (poplmark challenge) to the examples directory.