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;
2000-04-17 ago Pretty.chunks;
2000-03-15 ago removed Pretty.spc;
2000-03-09 ago quote tag arguments;
1999-09-29 ago new tsig components;
1999-07-23 ago replace assoc lists by Symtab.table;
1999-07-12 ago removed pretty_thm_no_hyps (again);
1999-07-08 ago added pretty_thm_no_hyps;
1999-07-03 ago oops;
1999-07-03 ago pretty_thm: include oracles (!) in hyps;
1999-06-28 ago cond_extern_table;
1999-03-17 ago qualify Theory.sign_of etc.;
1999-03-09 ago pretty_thm_no_quote;
1999-02-12 ago pretty_thm: quote terms (separately);
1999-01-12 ago show_tags;
1998-11-17 ago Pretty.spc;
1998-08-04 ago moved print_goals to locale.ML;
1998-06-05 ago print_data moved to theory.ML;
1998-05-20 ago tuned signature;
1998-04-03 ago tuned comments;
1997-12-29 ago pretty_name_space;
1997-12-19 ago adapted to new sort function;
1997-11-21 ago changed Sequence interface (now Seq, in seq.ML);
1997-11-20 ago removed data.ML (made part of sign.ML);
1997-11-20 ago moved Sign.print_sg to display.ML;
1997-11-12 ago tuned prths;
1997-11-04 ago added pretty_ctyp;
1997-10-24 ago tuned;
1997-10-20 ago tuned output;
1997-10-16 ago Eta-expansion of function declarations, for value polymorphism
1997-10-15 ago improved print_data;
1997-10-14 ago Sign.print_data;
1997-10-13 ago print_goals: optional output of const types (set show_consts);
1997-10-09 ago print_theory: added oracles;
1997-10-06 ago now uses new Sign.pretty_sort;
1997-09-11 ago removed print_goals_ref (which was broken anyway);
1997-07-22 ago added pretty_cterm;
1997-07-18 ago considered removal of print_goals_ref;
1997-04-18 ago print_goals: fixed show_sorts semantics;
1996-11-26 ago Eta-expansion of a function definition, for value polymorphism
1996-11-13 ago Removal of polymorphic equality via mem, subset, eq_set, etc
1996-03-20 ago New module for display/printing operations, taken from drule.ML