2007-05-31 ago simplified/unified list fold;
2006-12-05 ago thm/prf: separate official name vs. additional tags;
2006-10-31 ago fixed type signature of Type.varify
2006-09-21 ago member (op =);
2006-09-15 ago renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-08-02 ago tuned;
2006-06-11 ago avoid unqualified exception;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-26 ago tuned;
2006-04-13 ago ignore sorts of consts declarations;
2006-03-21 ago avoid polymorphic equality;
2006-02-06 ago Envir.(beta_)eta_contract;
2005-11-16 ago tuned Pattern.match/unify;
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-02 ago some 'assoc' etc. refactoring
2005-09-01 ago curried_lookup/update;
2005-08-01 ago replaced atless by term_ord;
2005-07-28 ago Sign.typ_unify;
2005-07-19 ago Logic.incr_tvar;
2005-07-15 ago tuned;
2005-07-13 ago (intermediate commit)
2005-04-21 ago Adapted to new interface of instantiation and unification / matching functions.
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-06-21 ago Merged in license change from Isabelle2004
2004-06-05 ago pretty_thm/goals_aux, pretty_flexpair: pp;
2004-06-01 ago removed obsolete sort 'logic';
2002-11-27 ago prop_of now returns proposition in beta-eta normal form.
2002-11-13 ago Improved function decompose.
2002-10-21 ago - reconstruct_proof no longer relies on TypeInfer.infer_types
2002-09-30 ago Fixed bug in expand_proof which caused indexes to be incremented incorrectly.
2002-07-10 ago expand_proof now also takes an optional term describing the proposition
2002-06-28 ago Added function prop_of' taking assumption context as an argument.
2002-05-11 ago - Tuned function mk_cnstrts
2002-02-06 ago Indexes of variables in expanded proofs are now incremented to avoid clashes.
2001-12-18 ago tuned Type.unify;
2001-11-19 ago Moved fastype to Envir.
2001-10-31 ago - Tuned add_cnstrt
2001-10-04 ago Fixed bug in decompose.
2001-09-28 ago - Exchanged % and %%
2001-08-31 ago tuned headers;
2001-08-31 ago Initial revision of tools for proof terms.