2010-05-15 ago less pervasive names from structure Thm;
2010-04-30 ago proper context for rule_by_tactic;
2010-04-26 ago eliminanated some unreferenced identifiers;
2010-03-06 ago removed unused term_lift_inst_rule (superceded by Subgoal.FOCUS etc.);
2009-11-25 ago normalized uncurry take/drop
2009-11-24 ago curried take/drop
2009-10-17 ago less pervasive names;
2009-07-06 ago structure Thm: less pervasive names;
2009-06-24 ago renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
2009-05-24 ago tuned whitespace
2009-03-17 ago renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
2008-12-31 ago qualified Term.rename_wrt_term;
2008-06-16 ago removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML);
2008-06-14 ago qualified old res_inst_tac variants;
2008-06-11 ago Drule.read_instantiate;
2008-04-12 ago rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-27 ago eliminated theory ProtoPure;
2008-01-21 ago Removed Logic.auto_rename.
2007-08-13 ago Lexicon.read_indexname/nat/variable;
2007-07-03 ago removed obsolete eta_long_tac;
2007-06-25 ago added eta_long_tac;
2007-06-03 ago cleaned up signature;
2007-05-31 ago simplified/unified list fold;
2007-04-04 ago added scanwords from library.ML (for obsolete rename_tac);
2007-04-03 ago renamed Variable.import to import_thms (avoid clash with Alice keywords);
2007-04-02 ago now exports distinct_subgoal_tac (needed by MetisAPI)
2007-02-26 ago moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2006-12-07 ago reorganized structure Tactic vs. MetaSimplifier;
2006-12-07 ago reorganized structure Goal vs. Tactic;
2006-08-02 ago renamed Syntax.indexname to Syntax.read_indexname;
2006-07-27 ago removed obsolete is_fact (cf. Thm.no_prems);
2006-07-26 ago Variable.import(T): result includes fixed types/terms;
2006-07-12 ago exported make_elim_preserve;
2006-06-19 ago eliminated freeze/varify in favour of Variable.import/export/trade;
2006-05-29 ago fixing a variable-clash bug in rule_by_tactic
2006-05-02 ago tidied and harmonized "params_of_state"
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-26 ago tuned;
2006-04-13 ago use conjunction stuff from conjunction.ML;
2006-03-04 ago tuned conj_curry;
2006-02-22 ago simplified Pure conjunction, based on actual const;
2006-02-15 ago sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
2006-02-08 ago introduced gen_distinct in place of distinct
2005-12-23 ago CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
2005-12-22 ago conjunction_tac: single goal;
2005-11-19 ago added CONJUNCTS: treat conjunction as separate sub-goals;
2005-11-10 ago renamed Thm.cgoal_of to Thm.cprem_of;
2005-10-28 ago accomodate simplified Thm.lift_rule;
2005-10-21 ago moved norm_hhf_rule, prove etc. to goal.ML;
2005-10-18 ago Simplifier.theory_context;
2005-10-15 ago tuned comments;
2005-09-20 ago slight adaptions to library changes
2005-09-06 ago introduced some new-style AList operations
2005-08-31 ago refer to theory instead of low-level tsig;
2005-07-28 ago norm_hhf_rule: Thm.adjust_maxidx_thm before Drule.gen_all;
2005-07-19 ago Logic.incr_tvar;
2005-07-13 ago export eq_brl;
2005-07-01 ago cterm_aconv: avoid rep_cterm;
2005-06-17 ago accomodate identification of type and theory;
2005-06-08 ago Fixed "axiom" generation for mixed locales with and without predicates.