2009-03-20 wenzelm 2009-03-20 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
2009-03-11 haftmann 2009-03-11 HOLogic.mk_set, HOLogic.dest_set
2009-03-05 haftmann 2009-03-05 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2008-09-22 haftmann 2008-09-22 fixed headers
2008-05-18 wenzelm 2008-05-18 oops -- pr_graph = Syntax.string_of_term; removed dead pr_matrix;
2008-05-18 wenzelm 2008-05-18 pr_matrix: proper context;
2008-05-12 krauss 2008-05-12 Measure functions can now be declared via special rules, allowing for a prolog-style generation of measure functions for a specific type.
2008-03-01 wenzelm 2008-03-01 use more antiquotations;
2007-11-06 krauss 2007-11-06 moved stuff about size change termination to its own session