src/Pure/tactic.ML
2006-04-13 wenzelm 2006-04-13 use conjunction stuff from conjunction.ML;
2006-03-04 wenzelm 2006-03-04 tuned conj_curry;
2006-02-22 wenzelm 2006-02-22 simplified Pure conjunction, based on actual const;
2006-02-15 wenzelm 2006-02-15 sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
2006-02-08 haftmann 2006-02-08 introduced gen_distinct in place of distinct
2005-12-23 wenzelm 2005-12-23 CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
2005-12-22 wenzelm 2005-12-22 conjunction_tac: single goal; added CONJUNCTS2, precise_conjunction_tac; removed smart_conjunction_tac;
2005-11-19 wenzelm 2005-11-19 added CONJUNCTS: treat conjunction as separate sub-goals;
2005-11-10 wenzelm 2005-11-10 renamed Thm.cgoal_of to Thm.cprem_of;
2005-10-28 wenzelm 2005-10-28 accomodate simplified Thm.lift_rule; tuned;
2005-10-21 wenzelm 2005-10-21 moved norm_hhf_rule, prove etc. to goal.ML; moved asm_rewrite_goal_tac to simplifier.ML;
2005-10-18 wenzelm 2005-10-18 Simplifier.theory_context;
2005-10-15 wenzelm 2005-10-15 tuned comments;
2005-09-20 haftmann 2005-09-20 slight adaptions to library changes
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);