src/Pure/display.ML
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.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-23 wenzelm 2004-06-23 tuned;
2004-06-22 wenzelm 2004-06-22 improved print_theory;
2004-06-21 wenzelm 2004-06-21 pretty_abbr;
2004-06-05 wenzelm 2004-06-05 pretty_thm/goals_aux, pretty_flexpair: pp;
2004-05-21 wenzelm 2004-05-21 adapted tsig/sg interface;
2004-04-22 wenzelm 2004-04-22 adapted Sign.rep_sg;
2004-04-16 berghofe 2004-04-16 Replaced quote by Library.quote, since quote now refers to Symbol.quote
2004-03-19 paulson 2004-03-19 Removing the datatype declaration of "order" allows the standard General.order to be used. Thus we can use Int.compare and String.compare instead of the slower home-grown versions.
2003-10-09 skalberg 2003-10-09 Added support for making constants final, that is, ensuring that no definition can be given later (useful for constants whose behaviour is fixed axiomatically rather than definitionally).
2003-08-31 skalberg 2003-08-31 Makes interactive proof scripting recognize the show_all_types flag.
2002-10-21 berghofe 2002-10-21 Changed handling of flex-flex constraints: now stored in separate tpairs field of theorem record.
2002-01-21 wenzelm 2002-01-21 reset show_hyps by default (in accordance to existing Isar practice);
2001-12-08 wenzelm 2001-12-08 tuned print_goals interfaces;
2001-11-06 wenzelm 2001-11-06 added goals_limit (from tctical.ML); added pretty_goals_aux, removed excessive variants of print_goals;
2001-11-06 wenzelm 2001-11-06 export pretty_thm_aux;
2001-10-22 wenzelm 2001-10-22 print_goals stuff is back (from locale.ML);
2001-08-15 wenzelm 2001-08-15 support for absolute namespace entry paths;
2000-12-23 wenzelm 2000-12-23 tuned output;
2000-09-17 wenzelm 2000-09-17 added print_thm(s)_sg;
2000-08-02 wenzelm 2000-08-02 use oracle flag from derivation;
2000-05-22 wenzelm 2000-05-22 show_consts no longer requires show_types;
2000-04-17 wenzelm 2000-04-17 Pretty.chunks;
2000-03-15 wenzelm 2000-03-15 removed Pretty.spc;
2000-03-09 wenzelm 2000-03-09 quote tag arguments;
1999-09-29 wenzelm 1999-09-29 new tsig components;
1999-07-23 wenzelm 1999-07-23 replace assoc lists by Symtab.table;
1999-07-12 wenzelm 1999-07-12 removed pretty_thm_no_hyps (again);
1999-07-08 wenzelm 1999-07-08 added pretty_thm_no_hyps;
1999-07-03 wenzelm 1999-07-03 oops;
1999-07-03 wenzelm 1999-07-03 pretty_thm: include oracles (!) in hyps;
1999-06-28 wenzelm 1999-06-28 cond_extern_table;
1999-03-17 wenzelm 1999-03-17 qualify Theory.sign_of etc.;
1999-03-09 wenzelm 1999-03-09 pretty_thm_no_quote;
1999-02-12 wenzelm 1999-02-12 pretty_thm: quote terms (separately);
1999-01-12 wenzelm 1999-01-12 show_tags; pretty/print_thms;
1998-11-17 wenzelm 1998-11-17 Pretty.spc;
1998-08-04 wenzelm 1998-08-04 moved print_goals to locale.ML;
1998-06-05 wenzelm 1998-06-05 print_data moved to theory.ML; print_theory: exclude theorems (no forward reference!);
1998-05-20 wenzelm 1998-05-20 tuned signature; added pretty_theory;
1998-04-03 wenzelm 1998-04-03 tuned comments;
1997-12-29 wenzelm 1997-12-29 pretty_name_space;
1997-12-19 wenzelm 1997-12-19 adapted to new sort function;
1997-11-21 wenzelm 1997-11-21 changed Sequence interface (now Seq, in seq.ML);
1997-11-20 wenzelm 1997-11-20 removed data.ML (made part of sign.ML);