src/HOL/Metis_Examples/Binary_Tree.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-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-02-14 blanchet 2014-02-14 merged 'List.map' and 'List.list.map'
2013-12-25 haftmann 2013-12-25 abolished slightly odd global lattice interpretation for min/max
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
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-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2011-12-01 blanchet 2011-12-01 tuning
2011-11-15 huffman 2011-11-15 avoid theorem references like 'semiring_norm(111)'
2011-06-06 blanchet 2011-06-06 tuned Metis examples