src/Pure/tactic.ML
2008-12-31 wenzelm 2008-12-31 qualified Term.rename_wrt_term;
2008-06-16 wenzelm 2008-06-16 removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML); removed obsolete rename_tac, rename_last_tac; renamed rename_params_tac to rename_tac;
2008-06-14 wenzelm 2008-06-14 qualified old res_inst_tac variants;
2008-06-11 wenzelm 2008-06-11 Drule.read_instantiate; Drule.types_sorts;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure;
2008-01-21 berghofe 2008-01-21 Removed Logic.auto_rename.
2007-08-13 wenzelm 2007-08-13 Lexicon.read_indexname/nat/variable;
2007-07-03 wenzelm 2007-07-03 removed obsolete eta_long_tac;
2007-06-25 wenzelm 2007-06-25 added eta_long_tac;
2007-06-03 wenzelm 2007-06-03 cleaned up signature;
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-04-04 wenzelm 2007-04-04 added scanwords from library.ML (for obsolete rename_tac);
2007-04-03 wenzelm 2007-04-03 renamed Variable.import to import_thms (avoid clash with Alice keywords);
2007-04-02 paulson 2007-04-02 now exports distinct_subgoal_tac (needed by MetisAPI)
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2006-12-07 wenzelm 2006-12-07 reorganized structure Tactic vs. MetaSimplifier;
2006-12-07 wenzelm 2006-12-07 reorganized structure Goal vs. Tactic;
2006-08-02 wenzelm 2006-08-02 renamed Syntax.indexname to Syntax.read_indexname;
2006-07-27 wenzelm 2006-07-27 removed obsolete is_fact (cf. Thm.no_prems);
2006-07-26 wenzelm 2006-07-26 Variable.import(T): result includes fixed types/terms;
2006-07-12 wenzelm 2006-07-12 exported make_elim_preserve;
2006-06-19 wenzelm 2006-06-19 eliminated freeze/varify in favour of Variable.import/export/trade;
2006-05-29 paulson 2006-05-29 fixing a variable-clash bug in rule_by_tactic
2006-05-02 paulson 2006-05-02 tidied and harmonized "params_of_state"
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-26 wenzelm 2006-04-26 tuned;
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).