src/HOL/Nominal/Examples/Weakening.thy
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-11 urbanc 2006-01-11 tuned proofs
2006-01-11 urbanc 2006-01-11 tuned the eqvt-proof
2005-12-05 urbanc 2005-12-05 tuned
2005-12-05 urbanc 2005-12-05 tuned
2005-12-04 urbanc 2005-12-04 tuned
2005-12-01 urbanc 2005-12-01 changed "fresh:" to "avoiding:" and cleaned up the weakening example
2005-11-30 urbanc 2005-11-30 adapted to the new nominal_induction
2005-11-28 urbanc 2005-11-28 some small tuning
2005-11-07 urbanc 2005-11-07 Initial commit of the theory "Weakening".