src/Pure/tactic.ML
2005-09-06 haftmann 2005-09-06 introduced some new-style AList operations
2005-08-31 wenzelm 2005-08-31 refer to theory instead of low-level tsig;
2005-07-28 wenzelm 2005-07-28 norm_hhf_rule: Thm.adjust_maxidx_thm before Drule.gen_all; removed prove_standard, prove_multi_standard;
2005-07-19 wenzelm 2005-07-19 Logic.incr_tvar;
2005-07-13 wenzelm 2005-07-13 export eq_brl;
2005-07-01 wenzelm 2005-07-01 cterm_aconv: avoid rep_cterm;
2005-06-17 wenzelm 2005-06-17 accomodate identification of type Sign.sg and theory;
2005-06-08 ballarin 2005-06-08 Fixed "axiom" generation for mixed locales with and without predicates.
2005-05-17 paulson 2005-05-17 added comment
2005-04-28 wenzelm 2005-04-28 added smart_conjunction_tac, prove_multi, prove_multi_standard;
2005-04-21 berghofe 2005-04-21 - Eliminated nodup_vars check. - Unification and matching functions now check types of term variables / sorts of type variables when applying a substitution. - Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list as argument, to allow for proper instantiation of theorems containing type variables with same name but different sorts.
2005-04-11 ballarin 2005-04-11 First release of interpretation commands.
2005-04-07 wenzelm 2005-04-07 Drule.add_used;
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.
2005-01-24 berghofe 2005-01-24 Added variant of eres_inst_tac that operates on indexnames instead of strings.
2005-01-24 paulson 2005-01-24 some rationalizing of res_inst_tac
2005-01-18 berghofe 2005-01-18 Added variants of instantiation functions that operate on pairs of type (indexname * string) instead of (string * string).
2004-07-08 wenzelm 2004-07-08 got rid of obsolete meta_simpset;
2004-06-30 skalberg 2004-06-30 Made simplification procedures simpset-aware.
2004-06-25 skalberg 2004-06-25 Merging the meta-simplifier with the Provers-simplifier. Next step: make the simplification procedure simpset-aware.
2004-04-26 wenzelm 2004-04-26 use Syntax.is_identifier;
2003-04-26 paulson 2003-04-26 catches exception DELETE
2002-10-17 paulson 2002-10-17 fixing the cut_tac method to work when there are no instantiations and the supplied theorems have premises
2002-09-05 paulson 2002-09-05 added checking so that (rename_tac "x y") is rejected, since "x y" is not an identifier
2002-05-07 wenzelm 2002-05-07 use eq_thm_prop instead of slightly inadequate eq_thm;
2002-01-24 wenzelm 2002-01-24 fixed subgoal_tac; fails on non-existent subgoal;
2002-01-17 wenzelm 2002-01-17 renamed norm_hhf to norm_hhf_rule; removed slow rewrite_cterm;
2002-01-16 wenzelm 2002-01-16 tune norm_hhf_tac;
2002-01-12 wenzelm 2002-01-12 renamed forall_elim_vars_safe to gen_all;
2001-12-14 wenzelm 2001-12-14 changed Thm.varifyT';
2001-11-29 wenzelm 2001-11-29 general type of delete_tagged_brl; tuned;
2001-11-21 wenzelm 2001-11-21 use tracing function for trace output;
2001-11-15 wenzelm 2001-11-15 prove: raise ERROR_MESSAGE;
2001-11-13 wenzelm 2001-11-13 prove: Envir.beta_norm;
2001-11-11 wenzelm 2001-11-11 added conjunction_tac;
2001-10-28 wenzelm 2001-10-28 tuned prove;
2001-10-27 wenzelm 2001-10-27 tuned prove; added prove_standard;
2001-10-27 wenzelm 2001-10-27 prove: primitive goal interface for internal use;
2001-10-25 wenzelm 2001-10-25 innermost_params;
2001-10-15 wenzelm 2001-10-15 qualify some names;
2001-10-14 wenzelm 2001-10-14 unified rewrite/rewrite_cterm/simplify interface;
2001-10-14 wenzelm 2001-10-14 tuned full_rewrite;
2001-10-04 wenzelm 2001-10-04 added full_rewrite_cterm;
2001-01-07 wenzelm 2001-01-07 tuned norm_hhf(_tac);
2001-01-06 wenzelm 2001-01-06 added norm_hhf(_tac);
2000-11-10 wenzelm 2000-11-10 added rewrite_goal_tac;
2000-11-07 berghofe 2000-11-07 moved rewriting functions from Drule to MetaSimplifier
2000-10-27 oheimb 2000-10-27 added instantiate_tac
2000-08-04 wenzelm 2000-08-04 added rename_params_tac;
2000-05-25 paulson 2000-05-25 res_inst_tac, etc., no longer print the "dest_state" message when the selected subgoal does not exist
2000-01-17 paulson 2000-01-17 Thm.instantiate no longer normalizes, but Drule.instantiate does
1999-09-25 wenzelm 1999-09-25 added fold_rule;
1999-09-06 oheimb 1999-09-06 added ftac, eatac, datac, fatac
1999-08-18 paulson 1999-08-18 new primitive rule permute_prems to underlie defer_tac and rotate_prems
1999-07-12 wenzelm 1999-07-12 removed metacuts_tac;
1999-07-10 wenzelm 1999-07-10 defer_tac: use try for general exn handling;
1999-03-17 wenzelm 1999-03-17 qualify Theory.sign_of etc.;
1998-11-26 nipkow 1998-11-26 Added filter_prems_tac