src/HOL/Metis_Examples/Trans_Closure.thy
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
2014-06-12 blanchet 2014-06-12 renamed Sledgehammer options
2014-01-30 blanchet 2014-01-30 renamed Sledgehammer options for symmetry between positive and negative versions
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-02-14 smolkas 2013-02-14 renamed sledgehammer_shrink to sledgehammer_compress
2013-01-03 blanchet 2013-01-03 use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
2012-11-06 blanchet 2012-11-06 renamed Sledgehammer option
2012-10-18 blanchet 2012-10-18 renamed Isar-proof related options + changed semantics of Isar shrinking
2011-12-24 haftmann 2011-12-24 adjusted to set/pred distinction by means of type constructor `set`
2011-06-06 blanchet 2011-06-06 tuned Metis examples