2012-03-18 wenzelm 2012-03-18 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-04-18 wenzelm 2011-04-18 pass plain Proof.context for pretty printing;
2011-04-18 wenzelm 2011-04-18 simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;
2011-04-16 wenzelm 2011-04-16 prefer local name spaces; tuned signatures; tuned;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2010-09-06 wenzelm 2010-09-06 turned show_hyps and show_tags into proper configuration option;
2010-09-03 wenzelm 2010-09-03 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
2010-09-03 wenzelm 2010-09-03 turned show_consts into proper configuration option;
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: 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;