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.
2005-05-17 ago added comment
2005-04-28 ago added smart_conjunction_tac, prove_multi, prove_multi_standard;
2005-04-21 ago - Eliminated nodup_vars check.
2005-04-11 ago First release of interpretation commands.
2005-04-07 ago Drule.add_used;
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2005-01-24 ago Added variant of eres_inst_tac that operates on indexnames instead of strings.
2005-01-24 ago some rationalizing of res_inst_tac
2005-01-18 ago Added variants of instantiation functions that operate on pairs of type
2004-07-08 ago got rid of obsolete meta_simpset;
2004-06-30 ago Made simplification procedures simpset-aware.
2004-06-25 ago Merging the meta-simplifier with the Provers-simplifier. Next step:
2004-04-26 ago use Syntax.is_identifier;
2003-04-26 ago catches exception DELETE
2002-10-17 ago fixing the cut_tac method to work when there are no instantiations and the
2002-09-05 ago added checking so that (rename_tac "x y") is rejected, since