2012-11-19 ago theorem status about oracles/futures is no longer printed by default;
2012-10-17 ago more formal markup;
2012-10-09 ago more explicit flags for facts table;
2012-10-03 ago more error positions;
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-08-29 ago renamed Position.str_of to;
2012-04-02 ago tuned signature;
2012-04-01 ago tuned signature;
2012-03-18 ago maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2012-03-17 ago proper naming of simprocs according to actual target context;
2012-03-14 ago source positions for locale and class expressions;
2012-03-09 ago tuned signature;
2012-03-03 ago canonical argument order for attribute application;
2011-11-28 ago separate module for concrete Isabelle markup;
2011-11-27 ago tuned;
2011-11-11 ago more scalable Proof_Context.prepare_sorts;
2011-11-09 ago tuned signature;
2011-11-09 ago sort assignment before simultaneous term_check, not isolated parse_term;
2011-11-03 ago more general Proof_Context.bind_propp, which allows outer parameters;
2011-11-03 ago tuned signature -- canonical argument order;
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-25 ago entity markup for "type", "constant";
2011-06-25 ago type classes: entity markup instead of old-style token markup;
2011-05-12 ago proper configuration options Proof_Context.debug and Proof_Context.verbose;
2011-04-28 ago literal facts `prop` may contain dummy patterns;
2011-04-28 ago eliminated slightly odd Proof_Context.bind_fixes;
2011-04-27 ago more precise positions via binding;
2011-04-27 ago tuned signature -- eliminated odd comment;
2011-04-27 ago more precise position information via Variable.add_fixes_binding;
2011-04-27 ago reorganized fixes as specialized (global) name space;
2011-04-23 ago clarified Consts.read_const;
2011-04-23 ago clarified Type.the_decl;
2011-04-23 ago more reports and error positions;
2011-04-19 ago split Type_Infer into early and late part, after Proof_Context;
2011-04-19 ago simplified check/uncheck interfaces: result comparison is hardwired by default;
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 tuned signature;
2011-04-17 ago markup facts via name space;
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 do not open ML structures;
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-16 ago tuned signature, disentangled dependencies;
2011-04-08 ago moved CONST syntax/translations to their proper place;
2011-04-08 ago discontinued special treatment of structure Lexicon;
2011-04-08 ago discontinued special treatment of structure Mixfix;
2011-04-07 ago simplified printer context: uniform externing and static token translations;
2011-04-06 ago eliminated odd object-oriented type_context/term_context;
2011-04-05 ago moved decode/parse operations to standard_syntax.ML;
2011-04-05 ago separate module for standard implementation of inner syntax operations;
2011-04-05 ago discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
2011-04-05 ago more precise propagation of reports/results through some inner syntax layers;
2011-04-03 ago added Position.reports convenience;
2011-03-30 ago accomodate autofix discipline of non-body context;
2011-03-30 ago more informative markup_free;