src/Pure/Proof/proof_rewrite_rules.ML
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-06-09 wenzelm 2011-06-09 more tight name invention -- avoiding old functions;
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-05-08 wenzelm 2010-05-08 renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
2010-03-30 krauss 2010-03-30 switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
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;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm; use exists_Const directly;
2008-11-15 wenzelm 2008-11-15 rewrite_proof: simplified simprocs (no name required); adapted PThm; fold_proof_atoms;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure;
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-04-13 haftmann 2007-04-13 canonical merge operations
2007-02-07 berghofe 2007-02-07 Added functions hhf_proof and un_hhf_proof.
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-07-11 wenzelm 2006-07-11 Name.invent_list;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-26 wenzelm 2006-04-26 tuned;
2006-04-25 wenzelm 2006-04-25 tuned;
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality; tuned;
2006-02-22 wenzelm 2006-02-22 rew: handle conjunctionI/D1/D2;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-11-16 wenzelm 2005-11-16 Term.betapplys;
2005-10-28 wenzelm 2005-10-28 renamed Goal constant to prop;
2005-10-21 wenzelm 2005-10-21 renamed triv_goal to goalI, rev_triv_goal to goalD;
2005-08-31 wenzelm 2005-08-31 refer to theory instead of low-level tsig;
2005-08-23 haftmann 2005-08-23 replaced ? by ??
2005-08-03 berghofe 2005-08-03 Adapted to new interface of thms_of_proof.
2005-07-15 wenzelm 2005-07-15 tuned fold on terms;
2005-07-13 haftmann 2005-07-13 (intermediate commit)
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
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.