src/Provers/hypsubst.ML
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;
2001-11-21 wenzelm 2001-11-21 use tracing function for trace output;
2001-01-07 wenzelm 2001-01-07 CHANGED_PROP;
2000-09-07 wenzelm 2000-09-07 tuned msg;
2000-08-28 wenzelm 2000-08-28 Method.SIMPLE_METHOD';
2000-08-17 wenzelm 2000-08-17 added 'symmetric' attribute;
2000-08-14 wenzelm 2000-08-14 added hypsubst;
2000-08-04 wenzelm 2000-08-04 added rev_eq_reflection; export stac; proof method setup: subst, hypsubst;
1997-12-23 paulson 1997-12-23 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
1997-11-26 paulson 1997-11-26 updated comment
1997-11-12 oheimb 1997-11-12 added thin_refl to hyp_subst_tac
1997-11-06 paulson 1997-11-06 hyp_subst_tac checks if the equality has type variables and uses a suitable method if so. Affects the dest_eq function
1997-07-22 paulson 1997-07-22 Removal of the tactical STATE
1997-03-07 paulson 1997-03-07 Prevent permutation of assumptions in hyp_subst_tac
1997-03-05 paulson 1997-03-05 Now uses rotate_tac and eta_contract_atom for greater speed
1996-11-12 paulson 1996-11-12 Removed a call to polymorphic mem
1996-11-01 paulson 1996-11-01 Replaced min by Int.min
1995-04-06 lcp 1995-04-06 Recoded with help from Toby to use rewriting instead of the subst rule -- the latter was too slow. But it must resort to the subst rule if the equality contains Vars.
1994-11-11 lcp 1994-11-11 Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
1994-11-02 lcp 1994-11-02 Provers/hypsubst: greatly simplified! No longer simulates a "eres_inst_tac" using rev_cut_eq; instead simply rotates the chosen equality to the end!
1994-10-19 lcp 1994-10-19 new comments explaining abandoned change
1994-01-18 lcp 1994-01-18 Updated refs to old Sign functions
1993-09-16 clasohm 1993-09-16 Initial revision