2015-04-01 wenzelm 2015-04-01 tuned signature;
2015-03-31 wenzelm 2015-03-31 clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
2014-08-19 wenzelm 2014-08-19 tuned signature -- moved type src to Token, without aliases;
2014-03-31 wenzelm 2014-03-31 some shortcuts for chunks, which sometimes avoid bulky string output;
2014-03-11 wenzelm 2014-03-11 tuned signature;
2014-03-10 wenzelm 2014-03-10 tuned signature -- prefer Name_Space.get with its builtin error;
2014-03-10 wenzelm 2014-03-10 abstract type Name_Space.table; clarified pretty_locale_deps: sort strings; clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;
2014-03-08 wenzelm 2014-03-08 modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121); proper context for global data; tuned signature;
2014-02-26 wenzelm 2014-02-26 tuned signature;
2013-08-20 wenzelm 2013-08-20 proper context;
2013-01-05 wenzelm 2013-01-05 more precise Local_Theory.level: 1 really means main target and >= 2 nested context; explicit target for context within global theory with after_close = exit to manage the 2 levels involved here; reject "(in target)" for nested contexts more reliably -- difficult to handle due to lack of nested reinit;
2012-11-30 wenzelm 2012-11-30 print formal entities with markup;
2012-04-03 wenzelm 2012-04-03 less intrusive visibility;
2012-04-03 wenzelm 2012-04-03 close context elements via Expression.cert/read_declaration; ensure visible context;
2012-04-01 wenzelm 2012-04-01 more general context command with auxiliary fixes/assumes etc.;
2012-04-01 wenzelm 2012-04-01 nothing specific about named target;
2012-04-01 wenzelm 2012-04-01 added Attrib.global_notes/local_notes/generic_notes convenience;
2012-03-21 wenzelm 2012-03-21 actually expose target context;
2012-03-21 wenzelm 2012-03-21 more explicit Toplevel.open_target/close_target; replaced 'context_includes' by 'context' 'includes'; tuned command descriptions;
2012-03-21 wenzelm 2012-03-21 tuned signature;
2012-03-21 wenzelm 2012-03-21 optional 'includes' element for long theorem statements; tuned signatures;
2012-03-21 wenzelm 2012-03-21 basic support for nested contexts including bundles; include multiple bundles; renamed "affirm" back to "assert" (cf. c4492c6bf450 which was motivated by obsolete Alice/ML); tuned signatures;
2012-03-20 wenzelm 2012-03-20 basic support for bundled declarations;