2012-03-18 ago comment;
2012-03-18 ago tuned;
2012-03-18 ago maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2011-11-25 ago prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import;
2011-11-09 ago sort assignment before simultaneous term_check, not isolated parse_term;
2011-07-13 ago sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML);
2011-06-08 ago more robust exception pattern General.Subscript;
2011-04-18 ago standardized aliases of operations on tsig;
2011-04-18 ago pass plain Proof.context for pretty printing;
2011-04-18 ago simplified pretty printing context, which is only required for certain kernel operations;
2011-04-17 ago added Binding.print convenience, which includes quote already;
2011-04-17 ago eliminated obsolete markup -- superseded by generic "entity" markup;
2011-04-17 ago report Name_Space.declare/define, relatively to context;
2011-04-16 ago modernized structure Proof_Context;
2011-04-16 ago prefer local name spaces;
2011-04-16 ago Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-08 ago simplified Pure syntax bootstrap;
2011-04-08 ago discontinued special treatment of structure Lexicon;
2011-04-08 ago discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
2011-04-08 ago discontinued special treatment of structure Mixfix;
2011-04-08 ago explicit structure Syntax_Trans;
2011-04-07 ago discontinued user-defined token translations;
2011-04-06 ago typed_print_translation: discontinued show_sorts argument;
2011-04-05 ago discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
2011-04-03 ago added Position.reports convenience;
2010-12-04 ago added Syntax.default_root;
2010-09-17 ago tuned signature of (Context_) variants;
2010-09-12 ago load type_infer.ML later -- proper context for Type_Infer.infer_types;
2010-09-12 ago common Type.appl_error, which also covers explicit constraints;
2010-09-05 ago turned show_brackets into proper configuration option;
2010-09-05 ago pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
2010-05-27 ago renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-28 ago more systematic naming of tsig operations;
2010-04-28 ago modernized/simplified Sign.set_defsort;
2010-04-16 ago replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix);
2010-04-15 ago misc tuning and simplification;
2010-03-27 ago disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
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-15 ago tuned;
2010-03-15 ago moved old Sign.intern_term to the place where it is still used;
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-03-03 ago authentic syntax for classes and type constructors;
2010-03-01 ago more uniform treatment of syntax for types vs. consts;
2010-02-27 ago read_class: perform actual read, with source position;
2010-02-25 ago provide direct access to the different kinds of type declarations;
2010-02-21 ago slightly more abstract syntax mark/unmark operations;
2010-02-21 ago authentic syntax for *all* term constants;
2010-02-18 ago more systematic treatment of qualified names derived from binding;
2010-02-15 ago discontinued unnamed infix syntax;
2010-01-04 ago discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
2010-01-04 ago dropped copy operation for legacy TheoryDataFun
2009-11-17 ago uniform new_group/reset_group;
2009-11-02 ago modernized structure Primitive_Defs;
2009-10-25 ago eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 ago maintain theory name via name space, not tags;
2009-10-25 ago more direct access to naming;
2009-10-25 ago allow name space entries to be "concealed" -- via binding/naming/local_theory;
2009-10-24 ago maintain position of formal entities via name space;