src/Pure/display.ML
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;
2005-06-09 ago print_theory: omit name spaces; NameSpace.extern_table;
2005-06-05 ago renamed const_deps to defs;
2005-05-31 ago Removed final_consts from theory data. Now const_deps deals with final
2005-05-31 ago renamed cond_extern to extern;
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-06-23 ago tuned;
2004-06-22 ago improved print_theory;
2004-06-21 ago pretty_abbr;
2004-06-05 ago pretty_thm/goals_aux, pretty_flexpair: pp;
2004-05-21 ago adapted tsig/sg interface;
2004-04-22 ago adapted Sign.rep_sg;
2004-04-16 ago Replaced quote by Library.quote, since quote now refers to Symbol.quote
2004-03-19 ago Removing the datatype declaration of "order" allows the standard General.order
2003-10-09 ago Added support for making constants final, that is, ensuring that no
2003-08-31 ago Makes interactive proof scripting recognize the show_all_types flag.
2002-10-21 ago Changed handling of flex-flex constraints: now stored in separate
2002-01-21 ago reset show_hyps by default (in accordance to existing Isar practice);
2001-12-08 ago tuned print_goals interfaces;
2001-11-06 ago added goals_limit (from tctical.ML);
2001-11-06 ago export pretty_thm_aux;
2001-10-22 ago print_goals stuff is back (from locale.ML);
2001-08-15 ago support for absolute namespace entry paths;
2000-12-23 ago tuned output;
2000-09-17 ago added print_thm(s)_sg;
2000-08-02 ago use oracle flag from derivation;
2000-05-22 ago show_consts no longer requires show_types;