src/Provers/hypsubst.ML
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