src/Provers/trancl.ML
2010-05-05 ago 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 ago Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
2009-10-22 ago map_range (and map_index) combinator
2009-09-29 ago tuned;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-07-30 ago trancl_tac etc.: back to static context -- problem was caused by bad solver in AFP/JiveDataStoreModel;
2009-07-30 ago qualified Subgoal.FOCUS;
2009-07-29 ago trans_tac: use theory from goal state, not the static context, which seems to be outdated under certain circumstances (why?);
2009-07-26 ago replaced old METAHYPS by FOCUS;
2009-03-01 ago use long names for old-style fold combinators;
2008-05-07 ago Terms returned by decomp are now eta-contracted.
2007-02-07 ago "prove" function now instantiates relation variable in order
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-08-02 ago Documentation added/improved.
2004-07-27 ago *** empty log message ***
2004-07-26 ago New prover for transitive and reflexive-transitive closure of relations.