2009-07-21 ago moved ProofContext.pretty_thm to Display.pretty_thm etc.;
2009-07-20 ago moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
2009-03-26 ago pretty_thm_aux etc.: explicit show_status flag;
2009-03-24 ago display derivation status of thms;
2009-03-10 ago pretty_full_theory: no longer display name prefix -- naming is far more complex now;
2009-03-01 ago replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
2009-02-11 ago Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
2009-01-21 ago removed Ids;
2008-12-13 ago Context.display_names;
2008-11-18 ago tuned;
2008-11-15 ago pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
2008-09-22 ago type thm: fully internal derivation, no longer exported;
2008-09-18 ago simplified oracle interface;
2008-09-18 ago added deriv.ML: Abstract derivations based on raw proof terms.
2008-06-20 ago type constructors now with markup
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 ago structure Display: less pervasive operations;
2008-04-13 ago tsig: removed unnecessary universal witness;
2008-04-12 ago rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-27 ago removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
2007-11-11 ago simplified Consts.dest;
2007-10-09 ago generic Syntax.pretty/string_of operations;
2007-10-04 ago replaced literal 'a by Name.aT;
2007-09-30 ago print_theory: observe Markup.internal_property of consts, discontinued special treatment of internal names elsewhere;
2007-09-20 ago avoid Theory.rep_theory;
2007-07-08 ago thm tag: list;
2007-07-07 ago pretty_goals_aux: subgoal markup;
2007-05-08 ago tuned;
2007-05-07 ago simplified DataFun interfaces;
2006-12-09 ago abbrevs: print original rhs;
2006-12-05 ago thm/prf: separate official name vs. additional tags;
2006-09-19 ago pretty_full_theory: suppress internal entities by default;
2006-07-27 ago removed obsolete pretty_thm_no_quote;
2006-07-26 ago moved pprint functions to Isar/proof_display.ML;
2006-07-11 ago Name.invent_list;
2006-06-07 ago renamed Type.(un)varifyT to Logic.(un)varifyT;
2006-05-23 ago made smlnj happy;
2006-05-23 ago pretty_full_theory: tuned output of definitions;
2006-05-22 ago pretty_full_theory: defs;
2006-05-16 ago more abstract interface to classes/arities;
2006-05-08 ago added raw_string_of_sort/typ/term;
2006-05-01 ago adapted arities;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-13 ago tuned comment;
2006-04-08 ago print_theory: print abbreviations nicely;
2006-03-21 ago subtract (op =);
2006-02-08 ago tuned;
2006-02-06 ago print_theory: const abbreviations;
2005-11-02 ago Consts.dest;
2005-10-27 ago consts: monomorphic;
2005-09-29 ago print_theory: discontinued final consts;
2005-09-17 ago pretty_thm_aux: ora masked by quick_and_dirty;
2005-09-17 ago pretty_thm_aux: aconv hyps;
2005-09-17 ago pretty_thm_aux: observe asms context;
2005-07-28 ago print_theory: const constraints;
2005-07-14 ago NameSpace.dest_table avoids duplicated extern;
2005-06-22 ago tuned;
2005-06-20 ago tuned;
2005-06-17 ago removed pretty_theory, pprint_theory (see context.ML or thy_info.ML);
2005-06-11 ago refer to name spaces values instead of names;