2007-08-20 ago tuned merge operations via pointer_eq;
2007-08-02 ago turned simp_depth_limit into configuration option;
2007-07-23 ago depth flag: plain bool ref;
2007-07-05 ago tuned;
2007-07-05 ago tuned goal conversion interfaces;
2007-07-03 ago moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
2007-06-03 ago merge_ss: plain merge of prems;
2007-05-31 ago simplified/unified list fold;
2007-05-10 ago moved some Drule operations to Thm (see more_thm.ML);
2007-05-09 ago simp_depth: now proper value in simpset (prevents problems with lost exception trace, enables multi-threaded simplification);
2007-04-16 ago canonical merge operations
2007-04-14 ago Morphism.transform/form;
2007-02-26 ago moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-02-06 ago trace/debug: avoid eager string concatenation;
2007-02-04 ago type simproc: explicitl dependency of morphism;
2007-01-31 ago changed cong alist - now using AList operations instead of overwrite_warn
2007-01-04 ago added mk_simproc': tuned interface;
2006-12-30 ago removed conditional combinator;
2006-12-07 ago reorganized structure Tactic vs. MetaSimplifier;
2006-12-05 ago thm/prf: separate official name vs. additional tags;
2006-11-30 ago qualified MetaSimplifier.norm_hhf(_protect);
2006-11-29 ago simplified Logic.count_prems;
2006-11-28 ago simplified '?' operator;
2006-11-24 ago ProofContext.init;
2006-11-10 ago introduces canonical AList functions for loop_tacs
2006-10-11 ago abandoned findrep
2006-10-09 ago Drule.lhs/rhs_of;
2006-09-21 ago member (op =);
2006-09-18 ago Thm.dest_arg;
2006-09-15 ago rrule: maintain 'extra' field for rule that contain extra vars outside elhs;
2006-08-03 ago tuned;
2006-08-02 ago normalized Proof.context/method type aliases;
2006-07-30 ago Thm.adjust_maxidx;
2006-07-27 ago moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
2006-07-25 ago use Term.add_vars instead of obsolete term_varnames;
2006-07-18 ago Term.declare_term_names;
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-07-08 ago tuned exception handling;
2006-07-06 ago add/del_simps: warning for inactive simpset (no context);
2006-06-06 ago tuned;
2006-05-11 ago tuned;
2006-04-29 ago tuned;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-03-21 ago gen_eq_set, remove (op =);
2006-02-26 ago rewrite_goals_rule_aux: actually use prems if present;
2006-02-15 ago rewrite_cterm: Thm.adjust_maxidx prevents unnecessary increments on rules;
2006-02-06 ago Envir.(beta_)eta_contract;
2006-01-04 ago trace_simp_depth_limit is 1 by default
2005-12-22 ago renamed imp_cong' to imp_cong_rule;
2005-11-19 ago simpset: added reorient field, set_reorient;
2005-10-21 ago moved various simplification tactics and rules to simplifier.ML;
2005-10-18 ago renamed set_context to context;
2005-10-17 ago added set/addloop' for simpset dependent loopers;
2005-10-04 ago minor tweaks for Poplog/ML;
2005-09-29 ago export debug_bounds;
2005-09-29 ago Simplifier now removes flex-flex constraints from theorem returned by prover.
2005-09-29 ago removed revert_bound;
2005-09-23 ago added mk_solver';
2005-09-20 ago slight adaptions to library changes
2005-09-02 ago some 'assoc' etc. refactoring