src/Pure/display.ML
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;
2005-07-28 wenzelm 2005-07-28 print_theory: const constraints;
2005-07-14 wenzelm 2005-07-14 NameSpace.dest_table avoids duplicated extern;
2005-06-22 wenzelm 2005-06-22 tuned;
2005-06-20 wenzelm 2005-06-20 tuned;
2005-06-17 wenzelm 2005-06-17 removed pretty_theory, pprint_theory (see context.ML or thy_info.ML); removed obsolete pretty_name_space; accomodate identification of type Sign.sg and theory;
2005-06-11 wenzelm 2005-06-11 refer to name spaces values instead of names;
2005-06-09 wenzelm 2005-06-09 print_theory: omit name spaces; NameSpace.extern_table;
2005-06-05 wenzelm 2005-06-05 renamed const_deps to defs; Type.freeze;
2005-05-31 obua 2005-05-31 Removed final_consts from theory data. Now const_deps deals with final constants.
2005-05-31 wenzelm 2005-05-31 renamed cond_extern to extern; NameSpace.path_of naming;
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.