src/Pure/tactic.ML
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-04-30 wenzelm 2010-04-30 proper context for rule_by_tactic;
2010-04-26 wenzelm 2010-04-26 eliminanated some unreferenced identifiers; tuned;
2010-03-06 wenzelm 2010-03-06 removed unused term_lift_inst_rule (superceded by Subgoal.FOCUS etc.);
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-10-17 wenzelm 2009-10-17 less pervasive names;
2009-07-06 wenzelm 2009-07-06 structure Thm: less pervasive names;
2009-06-24 wenzelm 2009-06-24 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported); renamed Variable.importT_thms to Variable.importT (again);
2009-05-24 haftmann 2009-05-24 tuned whitespace
2009-03-17 wenzelm 2009-03-17 renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.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.