src/HOL/Tools/rewrite_hol_proof.ML
2010-06-03 wenzelm 2010-06-03 do not open Proofterm, which is very ould style;
2010-06-01 berghofe 2010-06-01 Adapted to new format of proof terms containing explicit proofs of class membership.
2010-03-30 krauss 2010-03-30 switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2009-11-16 wenzelm 2009-11-16 generalized procs for rewrite_proof: allow skeleton; fulfill_norm_proof: always normalize result here, no re-normalization after filling;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Syntax;
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-04-02 berghofe 2009-04-02 Fixed bug in transformation of congruence rule for == (thanks to Andy Schropp for reporting this).
2008-11-16 wenzelm 2008-11-16 clarified Thm.proof_body_of vs. Thm.proof_of;
2008-11-15 wenzelm 2008-11-15 ProofSyntax.proof_of_term: removed obsolete disambiguisation table; adapted PThm;
2008-10-31 berghofe 2008-10-31 Removed argument prf2 in rewrite rules for equal_elim to make them applicable to eta-contracted proofs.
2008-09-17 wenzelm 2008-09-17 back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-06-18 wenzelm 2008-06-18 more antiquotations;
2008-04-13 wenzelm 2008-04-13 tuned;
2007-02-07 berghofe 2007-02-07 Fixed bug in mk_AbsP.
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-06-06 wenzelm 2006-06-06 tuned;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-02-11 berghofe 2005-02-11 Fully qualified refl and trans to avoid confusion with theorems in Lattice_Locales.partial_order.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2003-04-23 berghofe 2003-04-23 elim_cong now eta-expands proofs on the fly if required.
2002-09-30 berghofe 2002-09-30 - additional congruence rules for boolean operators - additional rewrite rules for exI / exE
2002-07-21 berghofe 2002-07-21 Rules for rewriting HOL proofs.