2015-07-26 wenzelm 2015-07-26 updated to infer_instantiate;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
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;
2012-02-26 haftmann 2012-02-26 dropped dead code
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 =)
2010-02-22 berghofe 2010-02-22 Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation contained variables bound by meta level quantifiers.
2009-10-22 haftmann 2009-10-22 map_range (and map_index) combinator
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 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?);
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2008-05-07 berghofe 2008-05-07 Terms returned by decomp are now eta-contracted.
2007-02-07 berghofe 2007-02-07 "prove" function now instantiates relation variable in order to avoid problems with higher-order unification. This allows relations to be encoded as binary predicates.
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-02 ballarin 2004-08-02 Documentation added/improved.
2004-07-27 ballarin 2004-07-27 *** empty log message ***
2004-07-26 ballarin 2004-07-26 New prover for transitive and reflexive-transitive closure of relations. - Code in Provers/trancl.ML - HOL: Simplifier set up to use it as solver