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;
2011-03-27 ago decode_term: some context-sensitive markup;
2011-03-27 ago tuned signatures;
2011-03-27 ago decode_term/disambig: report resolved term variables for the unique (!) result;
2010-12-04 ago added Syntax.default_root;
2010-12-02 ago configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
2010-09-20 ago renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-17 ago simplified some internal flags using Config.T instead of full-blown Proof_Data;
2010-09-17 ago tuned signature of (Context_) variants;
2010-09-17 ago allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
2010-09-13 ago tuned signature;
2010-09-13 ago Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
2010-09-12 ago Type_Infer.infer_types: plain error instead of kernel exception TYPE;
2010-09-12 ago load type_infer.ML later -- proper context for Type_Infer.infer_types;
2010-09-12 ago eliminated aliases of Type.constraint;
2010-09-07 ago highlight bad range of nested error (here from inner parsing);
2010-09-06 ago discontinued obsolete ProofContext.prems_limit;