2010-06-01 ago arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML;
2010-04-25 ago replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-18 ago pretty_full_theory: proper Syntax.init_pretty_global;
2009-10-25 ago eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 ago conceal consts via name space, not tags;
2009-10-24 ago renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 ago eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-09-30 ago eliminated redundant bindings;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-08-28 ago discontinued Display.pretty_ctyp/cterm etc.;
2009-08-28 ago removed obsolete print_ctyp, print_cterm;
2009-07-25 ago renamed structure Display_Goal to Goal_Display;
2009-07-23 ago clarified pretty_goals, pretty_thm_aux: plain context;
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 =);