src/Pure/tactic.ML
2015-03-19 wenzelm 2015-03-19 tuned comments;
2015-03-04 wenzelm 2015-03-04 tuned;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-12-20 wenzelm 2014-12-20 proper context for "net" tactics; avoid implicit Tactic.build_net -- make its operational behavior explicit in application;
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2013-05-29 wenzelm 2013-05-29 tuned signature -- more explicit flags for low-level Thm.bicompose;
2013-05-20 wenzelm 2013-05-20 more precise treatment of theory vs. Proof.context;
2013-04-03 wenzelm 2013-04-03 tuned -- Drule.comp_no_flatten includes Drule.incr_indexes already (NB: result should be deterministic by construction);
2012-11-26 wenzelm 2012-11-26 tuned signature; tuned;
2012-11-11 wenzelm 2012-11-11 tuned;
2012-10-16 wenzelm 2012-10-16 clarified defer/prefer: more specific errors;
2012-02-27 wenzelm 2012-02-27 simplified cut_tac (cf. d549b5b0f344);
2012-02-14 wenzelm 2012-02-14 eliminated odd/obsolete innermost_params (cf. a77ad6c86564, 3458b0e955ac);
2012-02-14 wenzelm 2012-02-14 eliminated obsolete aliases;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
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;