2011-04-16 ago modernized structure Proof_Context;
2011-01-14 ago tuned markup;
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-09 ago tuned markup;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2009-11-12 ago eliminated obsolete "internal" kind -- collapsed to unspecific "";
2009-11-08 ago print_theorems: suppress concealed (global) facts, unless "!" option is given;
2009-11-02 ago modernized structure Proof_Display;
2009-07-23 ago clarified pretty_goals, pretty_thm_aux: plain context;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-03-26 ago pretty_rule/print_results: no thm status here -- it is potentially slow and mostly uninformative/confusing as long as proofs are still unfinished;
2009-03-21 ago removed obsolete pprint operations;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 ago renamed NameSpace.base to NameSpace.base_name;
2009-01-21 ago removed Ids;
2008-09-12 ago more procise printing of fact names;
2008-09-02 ago no pervasive bindings;
2008-09-02 ago pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
2008-08-13 ago removed obsolete present_results;
2008-06-12 ago Facts.dest/export_static: content difference;
2008-05-18 ago pprint: proper global context via Syntax.init_pretty_global;
2008-04-16 ago pretty_theorems: use proper PureThy.facts_of;
2008-03-26 ago adapted to Context.thread_data interface;
2008-03-20 ago Facts.Named: include position;
2008-03-19 ago renamed datatype thmref to Facts.ref, tuned interfaces;
2007-10-09 ago generic Syntax.pretty/string_of operations;
2007-05-08 ago tuned ProofDisplay.pretty_full_theory;
2007-02-17 ago pretty_full_theory: expose in signature.
2007-01-19 ago moved ML context stuff to from Context to ML_Context;
2007-01-19 ago adapted ML context operations;
2006-11-21 ago moved theorem kinds from PureThy to Thm;
2006-10-07 ago added pretty_consts (from specification.ML);
2006-09-19 ago 'print_theory': bang option for full verbosity;
2006-08-02 ago moved debug option to proof_display.ML (again);
2006-07-29 ago rename legacy_pretty_thm to pretty_thm_legacy;
2006-07-27 ago ProofContext.legacy_pretty_thm;
2006-07-26 ago moved pprint functions to Isar/proof_display.ML;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-13 ago added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
2006-01-27 ago moved theorem tags from Drule to PureThy;
2005-10-04 ago minor tweaks for Poplog/ML;
2005-09-13 ago Printing of Isar proof elements etc.