2009-07-23 wenzelm 2009-07-23 clarified pretty_goals, pretty_thm_aux: plain context; explicit pretty_goals_without_context, print_goals_without_context; tuned;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-03-26 wenzelm 2009-03-26 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 wenzelm 2009-03-21 removed obsolete pprint operations; some explicit pp operations for toplevel pretty printing;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-09-12 wenzelm 2008-09-12 more procise printing of fact names;
2008-09-02 wenzelm 2008-09-02 no pervasive bindings; removed theory_results and related hook; print_results: ignore empty/internal kind -- like former theory_results;
2008-09-02 wenzelm 2008-09-02 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 wenzelm 2008-08-13 removed obsolete present_results; added theory_results, which is subject to hooks (formerly in present.ML);
2008-06-12 wenzelm 2008-06-12 Facts.dest/export_static: content difference; tuned;
2008-05-18 wenzelm 2008-05-18 pprint: proper global context via Syntax.init_pretty_global;
2008-04-16 wenzelm 2008-04-16 pretty_theorems: use proper PureThy.facts_of;
2008-03-26 wenzelm 2008-03-26 adapted to Context.thread_data interface;
2008-03-20 wenzelm 2008-03-20 Facts.Named: include position;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-05-08 wenzelm 2007-05-08 tuned ProofDisplay.pretty_full_theory;
2007-02-17 aspinall 2007-02-17 pretty_full_theory: expose in signature.
2007-01-19 wenzelm 2007-01-19 moved ML context stuff to from Context to ML_Context;
2007-01-19 wenzelm 2007-01-19 adapted ML context operations;
2006-11-21 wenzelm 2006-11-21 moved theorem kinds from PureThy to Thm;
2006-10-07 wenzelm 2006-10-07 added pretty_consts (from specification.ML);
2006-09-19 wenzelm 2006-09-19 'print_theory': bang option for full verbosity;
2006-08-02 wenzelm 2006-08-02 moved debug option to proof_display.ML (again); normalized Proof.context/method type aliases;
2006-07-29 wenzelm 2006-07-29 rename legacy_pretty_thm to pretty_thm_legacy;
2006-07-27 wenzelm 2006-07-27 ProofContext.legacy_pretty_thm;
2006-07-26 wenzelm 2006-07-26 moved pprint functions to Isar/proof_display.ML;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-13 wenzelm 2006-04-13 added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
2006-01-27 wenzelm 2006-01-27 moved theorem tags from Drule to PureThy;
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-09-13 wenzelm 2005-09-13 Printing of Isar proof elements etc.