src/Provers/order.ML
18 months ago wenzelm 2018-01-08 prefer qualified names;
2015-03-04 wenzelm 2015-03-04 tuned;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-04-16 wenzelm 2011-04-16 eliminated old List.nth; tuned;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-07-08 haftmann 2010-07-08 tuned titles
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 Seq.map) 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 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.