src/HOL/Nominal/Examples/Pattern.thy
2015-08-31 wenzelm 2015-08-31 prefer symbols;
2015-06-25 wenzelm 2015-06-25 tuned proofs;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2011-10-12 wenzelm 2011-10-12 tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
2011-09-03 haftmann 2011-09-03 tuned proof
2011-02-21 wenzelm 2011-02-21 modernized specifications;
2010-01-30 berghofe 2010-01-30 Adapted to changes in cases method.
2010-01-10 berghofe 2010-01-10 Adapted to changes in induct method.
2009-10-28 wenzelm 2009-10-28 eliminated hard tabulators, guessing at each author's individual tab-width;
2009-10-26 berghofe 2009-10-26 Added Pattern.thy to Nominal/Examples.