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;
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