2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2009-10-27 wenzelm 2009-10-27 eliminated some old folds;
2009-10-26 haftmann 2009-10-26 avoid upto if not needed
2009-10-22 haftmann 2009-10-22 map_range (and map_index) combinator
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-09-29 wenzelm 2009-09-29 tuned;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-30 wenzelm 2009-07-30 qualified Subgoal.FOCUS;
2009-07-26 wenzelm 2009-07-26 replaced old METAHYPS by FOCUS; eliminated homegrown SUBGOAL combinator -- beware of exception Subscript in body; modernized functor names; minimal tuning of sources; reactivated dead quasi.ML (ever used?);
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2008-12-31 wenzelm 2008-12-31 qualified Term.rename_wrt_term;
2008-05-07 berghofe 2008-05-07 Terms returned by decomp are now eta-contracted.
2007-09-25 ballarin 2007-09-25 Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
2007-09-18 ballarin 2007-09-18 Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
2007-07-05 wenzelm 2007-07-05 avoid polymorphic equality;
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2006-05-11 wenzelm 2006-05-11 avoid raw equality on type thm;
2006-03-11 wenzelm 2006-03-11 got rid of type;
2005-07-07 obua 2005-07-07 1) all theorems in Orderings can now be given as a parameter 2) new function Theory.defs_of 3) new functions Defs.overloading_info and Defs.is_overloaded
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-08-03 ballarin 2004-08-03 New transitivity reasoners for transitivity only and quasi orders.
2004-08-02 ballarin 2004-08-02 Documentation added/improved.
2004-03-08 ballarin 2004-03-08 Bug-fixes for transitivity reasoner.
2004-02-19 ballarin 2004-02-19 Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.