2015-07-09 wenzelm 2015-07-09 clarified specific use of inspect_contract: "any Bound variable will do" may render the term invalid for Term.fastype_of1 in inst_subst_tac (see also 7c3757fccf0e);
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-09 wenzelm 2014-11-09 proper context;
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-07-04 wenzelm 2014-07-04 more uniform names;
2014-06-11 Thomas Sewell 2014-06-11 Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.
2014-03-21 wenzelm 2014-03-21 more qualified names;
2013-05-24 wenzelm 2013-05-24 tuned signature;
2013-04-27 wenzelm 2013-04-27 uniform Proof.context for hyp_subst_tac;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-11-08 bulwahn 2012-11-08 hyp_subst_tac allows to pass an optional simpset to the internal simplifier call to avoid renamed bound variable warnings in the simplifier call
2012-06-19 Rafal Kolanski 2012-06-19 Updated comment to reflect current state.
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2011-11-28 wenzelm 2011-11-28 avoid stepping outside of context -- plain zero_var_indexes should be sufficient;
2011-11-24 wenzelm 2011-11-24 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-08-08 wenzelm 2011-08-08 misc tuning -- eliminated old-fashioned rep_thm;
2011-06-09 wenzelm 2011-06-09 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
2011-05-14 wenzelm 2011-05-14 modernized functor names; tuned;
2011-04-16 wenzelm 2011-04-16 more direct Thm.cprem_of (with exception THM instead of Subscript);
2011-04-16 wenzelm 2011-04-16 eliminated old List.nth; tuned;
2011-03-24 wenzelm 2011-03-24 more direct loose_bvar1; tuned;
2010-09-29 krauss 2010-09-29 backed out my old attempt at single_hyp_subst_tac (67cd6ed76446) It never was totally reliable, and better alternatives now exist (Subgoal.FOCUS).
2010-09-10 krauss 2010-09-10 use eta-contracted version for occurrence check (avoids possible non-termination) Test case: lemma "fwrap f = (%v. f v) ==> P f" apply clarify; pointed out by Thomas Sewell
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-04-29 wenzelm 2010-04-29 proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
2010-02-19 wenzelm 2010-02-19 renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
2009-03-13 wenzelm 2009-03-13 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2008-08-04 wenzelm 2008-08-04 meta_subst: xsymbols make it work with clean Pure;
2008-07-14 krauss 2008-07-14 single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
2008-05-24 wenzelm 2008-05-24 inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument; misc tuning -- more cterm operations, more qualified names;
2008-05-07 berghofe 2008-05-07 Added function for computing instantiation for the subst rule, which is used in vars_gen_hyp_subst_tac and blast_hyp_subst_tac to avoid problems with HO unification.
2007-07-22 wenzelm 2007-07-22 blast_hyp_subst_tac: plain bool argument;
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-11-07 wenzelm 2006-11-07 avoid handling of arbitrary exceptions;
2006-11-07 wenzelm 2006-11-07 simplified dest_eq; do not export debuging stuff; has_tvars: actually check all types within a term, not just its resulting type; tuned;
2006-10-11 haftmann 2006-10-11 slight type signature changes
2006-10-10 haftmann 2006-10-10 fixed intendation
2006-07-11 wenzelm 2006-07-11 Name.is_bound;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-10-18 wenzelm 2005-10-18 functor: no Simplifier argument; Simplifier.theory_context;
2005-08-01 wenzelm 2005-08-01 Term.is_bound;
2005-04-07 wenzelm 2005-04-07 improved comments;
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-12-16 paulson 2004-12-16 fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
2002-09-30 berghofe 2002-09-30 - eliminated thin_leading_eqs_tac - gen_hyp_subst_tac now uses asm_lr_simp_tac instead of asm_full_simp_tac, in order to avoid divergence of new simplifier
2001-12-05 wenzelm 2001-12-05 'symmetric' attribute moved to Pure/calculation.ML;