2006-01-19 ago setup: theory -> theory;
2005-11-16 ago Term.betapplys;
2005-10-28 ago renamed Goal constant to prop;
2005-10-21 ago renamed triv_goal to goalI, rev_triv_goal to goalD;
2005-08-31 ago refer to theory instead of low-level tsig;
2005-08-23 ago replaced ? by ??
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.