src/Provers/order.ML
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 Sign.sg;
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.