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;
2010-09-05 ago Syntax.standard_parse_term: eliminated redundant Pretty.pp;
2010-09-02 ago inner parsing: refrain from too many nested position reports to achieve more precise error feedback in the source;
2010-09-02 ago turned show_question_marks into proper configuration option;
2010-09-01 ago prefer regular print functions over slightly low-level Term.string_of_vname;
2010-08-26 ago renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
2010-08-11 ago tuned whitespace;
2010-08-08 ago proper context for Syntax.parse_token;
2010-08-08 ago prefer where a proper context is available -- notably for "inner" entities;
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
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-29 ago read_const: disallow internal names as usual in visible Isar text;
2010-04-29 ago ProofContext.read_const: allow for type constraint (for fixed variable);
2010-04-29 ago allow mixfix syntax for fixes within a proof body -- should now work thanks to fully authentic syntax;
2010-04-28 ago localized default sort;
2010-04-28 ago more systematic naming of tsig operations;
2010-04-28 ago get_sort: minimize sorts given in the text, while keeping those from the context unchanged (the latter are preferred);
2010-04-27 ago monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
2010-04-15 ago get_sort: suppress dummyS from input;
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-06 ago provide ProofContext.def_type depending on "pattern" mode;