src/Pure/display.ML
2010-06-01 wenzelm 2010-06-01 arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML; misc tuning;
2010-04-25 wenzelm 2010-04-25 replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-18 wenzelm 2010-02-18 pretty_full_theory: proper Syntax.init_pretty_global;
2009-10-25 wenzelm 2009-10-25 eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 wenzelm 2009-10-25 conceal consts via name space, not tags;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 wenzelm 2009-10-24 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
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 =);