2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-07-04 ago added generalize;
2006-06-17 ago Term.internal;
2006-06-13 ago removed weak_eq_thm;
2006-06-12 ago tuned Seq/Envir/Unify interfaces;
2006-06-11 ago outer_params: Syntax.dest_internal;
2006-06-05 ago support embedded terms;
2006-06-01 ago Tiny code cleanup
2006-05-26 ago forall_intr_list: do not ignore errors;
2006-05-01 ago added sort_triv;
2006-04-29 ago added unconstrainTs;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-13 ago added equal_elim_rule2;
2006-03-04 ago added mk_conjunction;
2006-02-22 ago removed rename_indexes_wrt;
2006-02-15 ago added distinct_prems_rl;
2006-02-06 ago Envir.(beta_)eta_contract;
2006-02-03 ago removed add/del_rules;
2006-01-28 ago added equals_cong;
2006-01-27 ago moved theorem tags from Drule to PureThy;
2006-01-25 ago abs_def: improved error;
2006-01-21 ago simplified type attribute;
2006-01-10 ago added declaration_attribute;
2005-12-31 ago tuned forall_intr_vars;
2005-12-23 ago conj_elim_precise: proper treatment of nested conjunctions;
2005-12-22 ago fixed has_internal;
2005-12-08 ago removed Syntax.deskolem;
2005-12-02 ago abs_def: beta/eta contract lhs;
2005-11-25 ago forall_conv: limit prefix;
2005-11-22 ago export map_tags;
2005-11-19 ago removed conj_mono;
2005-11-16 ago added protect_cong, cong_mono_thm;
2005-11-09 ago added fold_terms;
2005-11-08 ago removed impose_hyps, satisfy_hyps;
2005-10-28 ago added incr_indexes;
2005-10-21 ago renamed triv_goal to goalI, rev_triv_goal to goalD;
2005-09-29 ago Optimized and exported flexflex_unique.
2005-09-26 ago moved disambiguate_frees to ProofKernel;
2005-09-26 ago added Drule.disambiguate_frees : thm -> thm
2005-09-12 ago introduced new-style AList operations
2005-08-31 ago refer to theory instead of low-level tsig;
2005-08-01 ago replaced atless by term_ord;
2005-07-28 ago tuned gen_all, forall_elim_list, implies_intr_list, standard;
2005-07-15 ago tuned fold on terms;
2005-07-13 ago (fix for an accidental commit)
2005-07-13 ago (intermediate commit)
2005-07-06 ago Thm.full_prop_of;
2005-07-04 ago tuned;
2005-06-29 ago added implies_intr_hyps (from thm.ML);
2005-06-17 ago accomodate identification of type and theory;
2005-05-10 ago new cterm primitives
2005-05-04 ago Added eta_long_conversion.
2005-04-28 ago added plain_prop_of;
2005-04-21 ago - Eliminated nodup_vars check.
2005-04-07 ago added add_used; include tpairs;
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-22 ago Lucas - fixed bug in zero_var_indexes: it was ignoring vars in the flex-flex pairs. These are now taken into account.
2005-02-13 ago Deleted Library.option type.
2005-02-03 ago new treatment of demodulation in proof reconstruction