2010-06-01 ago outer_constraints with original variable names, to ensure that argsP is consistent with args
2010-05-09 ago just one version of Thm.unconstrainT, which affects all variables;
2010-05-09 ago added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
2010-03-21 ago Logic.mk_of_sort convenience;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2009-09-30 ago eliminated redundant bindings;
2009-09-29 ago modernized Balanced_Tree;
2009-07-16 ago tuned incr_tvar_same;
2009-07-16 ago export incr_tvar_same;
2009-07-16 ago use structure Same;
2009-07-16 ago removed obsolete/unused legacy_varify;
2009-07-15 ago tuned comment;
2009-07-14 ago removed obsolete/unused legacy_unvarify;
2009-07-10 ago tuned varify/unvarify: use Term_Subst.map_XXX combinators;
2009-07-06 ago renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
2009-03-16 ago substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 ago renamed NameSpace.base to NameSpace.base_name;
2008-12-31 ago qualified Term.rename_wrt_term;
2008-11-20 ago Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-10-01 ago tuned comments;
2008-06-23 ago added all, is_all;
2008-03-27 ago eliminated theory ProtoPure;
2008-01-21 ago Removed Logic.auto_rename.
2007-10-04 ago replaced literal 'a by Name.aT;
2007-08-14 ago moved support for primitive defs to primitive_defs.ML;
2007-07-05 ago simplified has_meta_prems;
2007-06-19 ago balanced conjunctions;
2007-06-13 ago removed unused is_atomic;
2007-06-04 ago added is_atomic;
2007-05-09 ago removed unused mk_cond_defpair;
2006-11-29 ago simplified Logic.count_prems;
2006-11-24 ago added type_map;
2006-10-13 ago Repaired strip_assums_hyp (now also works for goals not
2006-10-07 ago removed is_equals, is_implies;
2006-09-19 ago added name_classrel/arities/arity;
2006-09-15 ago renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-06-13 ago (un)varify: tuned exceptions;
2006-06-07 ago renamed Type.(un)varifyT to Logic.(un)varifyT;
2006-06-05 ago support embedded terms;
2006-04-13 ago added dest_conjunction_list;
2006-04-11 ago added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
2006-04-10 ago Term.itselfT;
2006-02-22 ago simplified Pure conjunction, based on actual const;
2006-02-18 ago dest_def: tuned error msg;
2006-02-16 ago dest_def: actually return beta-eta contracted equation;
2006-02-07 ago renamed gen_duplicates to duplicates;
2006-02-06 ago added generic dest_def (mostly from theory.ML);
2006-01-24 ago added dest_all;
2005-12-23 ago added mk_conjunction_list2;
2005-12-22 ago mk_conjunction: proper treatment of bounds;
2005-11-25 ago tuned;
2005-11-16 ago tuned;
2005-10-28 ago renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-08-18 ago optimization to incr_indexes?
2005-07-19 ago incr_tvar (from term.ML), incr_indexes: avoid garbage;
2005-07-15 ago tuned;
2005-07-14 ago occs no longer infix (structure not open);
2005-05-31 ago added nth_prem;