src/Pure/Proof/proof_rewrite_rules.ML
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2003-04-23 berghofe 2003-04-23 elim_vars now handles both Vars and Frees.
2002-10-14 nipkow 2002-10-14 Ported find_intro/elim to Isar.
2002-09-30 berghofe 2002-09-30 Added function elim_vars.
2002-07-10 berghofe 2002-07-10 - Moved abs_def to drule.ML - elim_defs now takes a boolean argument which controls the automatic expansion of theorems mentioning constants whose definitions are eliminated
2002-06-28 berghofe 2002-06-28 Additional rule for rewriting on ==.
2002-05-31 berghofe 2002-05-31 Changed interface of Pattern.rewrite_term.
2002-02-20 berghofe 2002-02-20 New function for eliminating definitions in proof term.
2002-02-02 berghofe 2002-02-02 Rewrite procedure now works for both compact and full proof objects.
2001-11-19 berghofe 2001-11-19 Added setup.
2001-10-31 berghofe 2001-10-31 Additional rules for simplifying inside "Goal"
2001-09-28 berghofe 2001-09-28 Exchanged % and %%.
2001-08-31 wenzelm 2001-08-31 tuned headers;
2001-08-31 berghofe 2001-08-31 Initial revision of tools for proof terms.