2005-08-03 ago Adapted to new interface of thms_of_proof.
2005-07-15 ago tuned fold on terms;
2005-07-13 ago (intermediate commit)
2005-04-21 ago superceded by Pure.thy and CPure.thy;
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
2003-04-23 ago elim_vars now handles both Vars and Frees.
2002-10-14 ago Ported find_intro/elim to Isar.
2002-09-30 ago Added function elim_vars.
2002-07-10 ago - Moved abs_def to drule.ML
2002-06-28 ago Additional rule for rewriting on ==.
2002-05-31 ago Changed interface of Pattern.rewrite_term.
2002-02-20 ago New function for eliminating definitions in proof term.
2002-02-02 ago Rewrite procedure now works for both compact and full proof objects.
2001-11-19 ago Added setup.
2001-10-31 ago Additional rules for simplifying inside "Goal"
2001-09-28 ago Exchanged % and %%.
2001-08-31 ago tuned headers;
2001-08-31 ago Initial revision of tools for proof terms.