src/Pure/display.ML
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-08-28 wenzelm 2009-08-28 discontinued Display.pretty_ctyp/cterm etc.;
2009-08-28 wenzelm 2009-08-28 removed obsolete print_ctyp, print_cterm;
2009-07-25 wenzelm 2009-07-25 renamed structure Display_Goal to Goal_Display;
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 moved ProofContext.pretty_thm to Display.pretty_thm etc.; explicit old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.; removed some very old thm print operations;
2009-07-20 wenzelm 2009-07-20 moved pretty_goals etc. to Display_Goal (required by tracing tacticals); load display.ML after assumption.ML, to accomodate proper contextual theorem display;
2009-03-26 wenzelm 2009-03-26 pretty_thm_aux etc.: explicit show_status flag;
2009-03-24 wenzelm 2009-03-24 display derivation status of thms;
2009-03-10 wenzelm 2009-03-10 pretty_full_theory: no longer display name prefix -- naming is far more complex now;
2009-03-01 wenzelm 2009-03-01 replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already); minor tuning according to Isabelle coding conventions;
2009-02-11 kleing 2009-02-11 Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-12-13 wenzelm 2008-12-13 Context.display_names;
2008-11-18 wenzelm 2008-11-18 tuned;
2008-11-15 wenzelm 2008-11-15 pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
2008-09-22 wenzelm 2008-09-22 type thm: fully internal derivation, no longer exported;
2008-09-18 wenzelm 2008-09-18 simplified oracle interface;
2008-09-18 wenzelm 2008-09-18 added deriv.ML: Abstract derivations based on raw proof terms.
2008-06-20 haftmann 2008-06-20 type constructors now with markup
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-04-13 wenzelm 2008-04-13 tsig: removed unnecessary universal witness;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-27 wenzelm 2008-03-27 removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
2007-11-11 wenzelm 2007-11-11 simplified Consts.dest;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-04 wenzelm 2007-10-04 replaced literal 'a by Name.aT;
2007-09-30 wenzelm 2007-09-30 print_theory: observe Markup.internal_property of consts, discontinued special treatment of internal names elsewhere;
2007-09-20 wenzelm 2007-09-20 avoid Theory.rep_theory;
2007-07-08 wenzelm 2007-07-08 thm tag: Markup.property list;
2007-07-07 wenzelm 2007-07-07 pretty_goals_aux: subgoal markup; print_goals etc.: moved old version to old_goals.ML, removed hooks; tuned;
2007-05-08 wenzelm 2007-05-08 tuned;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2006-12-09 wenzelm 2006-12-09 abbrevs: print original rhs;
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-09-19 wenzelm 2006-09-19 pretty_full_theory: suppress internal entities by default;
2006-07-27 wenzelm 2006-07-27 removed obsolete pretty_thm_no_quote;
2006-07-26 wenzelm 2006-07-26 moved pprint functions to Isar/proof_display.ML;
2006-07-11 wenzelm 2006-07-11 Name.invent_list;
2006-06-07 wenzelm 2006-06-07 renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;
2006-05-23 wenzelm 2006-05-23 made smlnj happy;
2006-05-23 wenzelm 2006-05-23 pretty_full_theory: tuned output of definitions;
2006-05-22 wenzelm 2006-05-22 pretty_full_theory: defs;
2006-05-16 wenzelm 2006-05-16 more abstract interface to classes/arities;
2006-05-08 wenzelm 2006-05-08 added raw_string_of_sort/typ/term;
2006-05-01 wenzelm 2006-05-01 adapted arities;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-13 wenzelm 2006-04-13 tuned comment;
2006-04-08 wenzelm 2006-04-08 print_theory: print abbreviations nicely;
2006-03-21 wenzelm 2006-03-21 subtract (op =);
2006-02-08 wenzelm 2006-02-08 tuned;
2006-02-06 wenzelm 2006-02-06 print_theory: const abbreviations;
2005-11-02 wenzelm 2005-11-02 Consts.dest;
2005-10-27 wenzelm 2005-10-27 consts: monomorphic;
2005-09-29 wenzelm 2005-09-29 print_theory: discontinued final consts;
2005-09-17 wenzelm 2005-09-17 pretty_thm_aux: ora masked by quick_and_dirty;
2005-09-17 wenzelm 2005-09-17 pretty_thm_aux: aconv hyps;
2005-09-17 wenzelm 2005-09-17 pretty_thm_aux: observe asms context;