2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-03 ago tuned;
2012-10-03 ago allow position constraints to coexist with 0 or 1 sort constraints;
2012-10-01 ago report sort assignment of visible type variables;
2012-03-19 ago clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);
2012-03-18 ago maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2012-03-11 ago more direct Name_Space.defined_entry;
2012-02-15 ago renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2011-11-28 ago separate module for concrete Isabelle markup;
2011-11-27 ago tuned;
2011-11-12 ago tuned markup -- prefer user-perspective;
2011-11-11 ago discontinued entity text color, notably historic red for classes;
2011-11-09 ago tuned;
2011-11-07 ago tuned;
2011-10-28 ago slightly more explicit/syntactic modelling of morphisms;
2011-07-12 ago more thorough Variable.check_name: Binding.check for logical entities within the term language;
2011-06-09 ago tuned signature: Name.invent and Name.invent_names;
2011-06-09 ago simplified Name.variant -- discontinued builtin fold_map;
2011-04-27 ago clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
2011-04-27 ago tuned signature -- eliminated odd comment;
2011-04-27 ago more informative markup for fixed variables (via name space entry);
2011-04-27 ago reorganized fixes as specialized (global) name space;
2011-04-27 ago more uniform Variable.add_frees/add_fixed etc.;
2011-04-16 ago modernized structure Proof_Context;
2011-04-16 ago tuned signature, disentangled dependencies;
2010-10-25 ago recovered some odd two-dimensional layout;
2010-09-24 ago modernized structure Ord_List;
2010-09-12 ago load type_infer.ML later -- proper context for Type_Infer.infer_types;
2010-08-27 ago more careful treatment of context visibility flag wrt. spurious warnings;
2010-05-27 ago renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-04 ago simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-30 ago renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
2009-11-25 ago normalized uncurry take/drop
2009-11-24 ago curried take/drop
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-10-21 ago curried inter as canonical list operation (beware of argument order)
2009-10-21 ago dropped redundant gen_ prefix
2009-10-20 ago replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-09-30 ago eliminated redundant bindings;
2009-07-30 ago Variable.importT/import: return full instantiations, tuned;
2009-07-26 ago Variable.focus: named parameters;
2009-07-09 ago renamed structure TermSubst to Term_Subst;
2009-06-24 ago renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
2009-03-28 ago replaced add_binds by singleton bind_term;
2009-01-21 ago eliminated obsolete var morphism;
2008-12-31 ago Term.declare_typ_names, Term.declare_term_frees;
2008-12-04 ago cleaned up binding module and related code
2008-10-16 ago maintain sort occurrences of declared terms;
2008-06-19 ago added declare_typ;
2008-06-10 ago focus: actually declare constraints for local parameters;
2008-04-17 ago variant_fixes: preserve internal state, mark skolem only for body mode;
2007-12-07 ago exported declare_names
2007-11-07 ago refined notion of consts within the local scope;
2007-11-06 ago added is_const/declare_const for local scope of fixes/consts;
2007-10-16 ago add_bind: close_schematic_term;
2007-10-04 ago replaced literal 'a by Name.aT;
2007-09-29 ago maintain maxidx (analogous to name context);
2007-09-26 ago declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
2007-09-24 ago added polymorphic_types;