src/Provers/quasi.ML
2010-07-08 haftmann 2010-07-08 tuned titles
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 explicit indication of Unsynchronized.ref;
2009-07-30 wenzelm 2009-07-30 trancl_tac etc.: back to static context -- problem was caused by bad solver in AFP/JiveDataStoreModel;
2009-07-30 wenzelm 2009-07-30 qualified Subgoal.FOCUS;
2009-07-29 wenzelm 2009-07-29 trans_tac: use theory from goal state, not the static context, which seems to be outdated under certain circumstances (why?);
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?);
2008-12-31 wenzelm 2008-12-31 qualified Term.rename_wrt_term;
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2006-03-11 wenzelm 2006-03-11 got rid of type Sign.sg;
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.