2010-05-04 ago proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
2010-04-28 ago more systematic naming of tsig operations;
2010-04-28 ago export Type.minimize_sort;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-09 ago aliases for class/type/const;
2010-03-09 ago added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
2010-02-25 ago provide direct access to the different kinds of type declarations;
2010-01-05 ago avoid exporting Type.build_tsig
2009-12-02 ago exported build_tsig
2009-11-21 ago explicitly mark some legacy freeze operations;
2009-11-09 ago locale_const/target_notation: uniform use of Term.aconv_untyped;
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-10-25 ago eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-24 ago maintain position of formal entities via name space;
2009-10-24 ago maintain explicit name space kind;
2009-10-24 ago renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 ago eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-09-30 ago eliminated redundant bindings;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-09-23 ago Correct chasing of type variable instantiations during type unification.
2009-07-17 ago eq_type: special case for empty environment;
2009-07-06 ago witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables;
2009-03-07 ago replace old bstring by binding for logical primitives: class, type, const etc.;
2008-12-31 ago moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 ago moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
2008-12-30 ago varify: regular name context;
2008-12-05 ago dropped NameSpace.declare_base
2008-12-04 ago cleaned up binding module and related code
2008-08-27 ago type Properties.T;
2008-06-21 ago the_tags: explicit error message;
2008-06-20 ago type constructors now with markup
2008-06-19 ago add_abbrev: check tfrees of rhs, not tvars (addresses a lapse introduced in 1.65);
2008-04-15 ago simplified hide_XXX interfaces;
2008-04-13 ago tsig: removed unnecessary universal witness;
2008-04-02 ago canonical meet_sort operation
2008-03-19 ago Type.lookup now curried; typ_of_sort
2007-11-10 ago similar_types: uniform treatment of TFrees/TVars;
2007-11-07 ago tuned signature;
2007-10-11 ago replaced Term.equiv_types by Type.similar_types;
2007-10-04 ago replaced literal 'a by Name.aT;
2007-08-30 ago maintain mode in context (get/set/restore_mode);
2007-08-14 ago type mode: models certification mode (default, syntax, abbrev);
2007-07-08 ago replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-05-31 ago simplified/unified list fold;
2006-12-29 ago Sorts.minimal_classes;
2006-12-15 ago avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-10-31 ago fixed type signature of Type.varify
2006-10-10 ago gen_rem(s) abandoned in favour of remove / subtract
2006-09-21 ago serial numbers for types;
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-07 ago renamed Type.(un)varifyT to Logic.(un)varifyT;
2006-05-22 ago export raw_unifys, could_unifys;
2006-05-20 ago export raw_matches;
2006-05-16 ago more abstract interface to classes/arities;
2006-05-05 ago replaced Sorts.DOMAIN by general Sorts.CLASS_ERROR;
2006-05-02 ago tuned;
2006-04-30 ago build classes/arities: refer to operations in sorts.ML;
2006-04-25 ago added inter_sort;
2006-03-21 ago avoid polymorphic equality;