src/Pure/display.ML
Fri, 28 Aug 2009 18:19:07 +0200 wenzelm removed obsolete print_ctyp, print_cterm;
Sat, 25 Jul 2009 10:31:27 +0200 wenzelm renamed structure Display_Goal to Goal_Display;
Thu, 23 Jul 2009 16:52:16 +0200 wenzelm clarified pretty_goals, pretty_thm_aux: plain context;
Tue, 21 Jul 2009 00:56:19 +0200 wenzelm moved ProofContext.pretty_thm to Display.pretty_thm etc.;
Mon, 20 Jul 2009 21:20:09 +0200 wenzelm moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
Thu, 26 Mar 2009 15:18:50 +0100 wenzelm pretty_thm_aux etc.: explicit show_status flag;
Tue, 24 Mar 2009 21:24:53 +0100 wenzelm display derivation status of thms;
Tue, 10 Mar 2009 16:43:59 +0100 wenzelm pretty_full_theory: no longer display name prefix -- naming is far more complex now;
Sun, 01 Mar 2009 14:45:23 +0100 wenzelm replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
Wed, 11 Feb 2009 16:03:10 +1100 kleing Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Sat, 13 Dec 2008 15:00:39 +0100 wenzelm Context.display_names;
Tue, 18 Nov 2008 18:25:45 +0100 wenzelm tuned;
Sat, 15 Nov 2008 21:31:21 +0100 wenzelm pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
Mon, 22 Sep 2008 15:26:07 +0200 wenzelm type thm: fully internal derivation, no longer exported;
Thu, 18 Sep 2008 19:39:44 +0200 wenzelm simplified oracle interface;
Thu, 18 Sep 2008 14:06:56 +0200 wenzelm added deriv.ML: Abstract derivations based on raw proof terms.
Fri, 20 Jun 2008 21:00:26 +0200 haftmann type constructors now with markup
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Sat, 17 May 2008 13:54:30 +0200 wenzelm structure Display: less pervasive operations;
Sun, 13 Apr 2008 16:40:02 +0200 wenzelm tsig: removed unnecessary universal witness;
Sat, 12 Apr 2008 17:00:35 +0200 wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
Thu, 27 Mar 2008 14:41:07 +0100 wenzelm removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
Sun, 11 Nov 2007 20:29:05 +0100 wenzelm simplified Consts.dest;
Tue, 09 Oct 2007 00:20:13 +0200 wenzelm generic Syntax.pretty/string_of operations;
Thu, 04 Oct 2007 20:29:24 +0200 wenzelm replaced literal 'a by Name.aT;
Sun, 30 Sep 2007 16:20:35 +0200 wenzelm print_theory: observe Markup.internal_property of consts, discontinued special treatment of internal names elsewhere;
Thu, 20 Sep 2007 20:56:33 +0200 wenzelm avoid Theory.rep_theory;
Sun, 08 Jul 2007 19:52:05 +0200 wenzelm thm tag: Markup.property list;
Sat, 07 Jul 2007 18:39:14 +0200 wenzelm pretty_goals_aux: subgoal markup;
Tue, 08 May 2007 21:02:26 +0200 wenzelm tuned;
Mon, 07 May 2007 00:49:59 +0200 wenzelm simplified DataFun interfaces;
Sat, 09 Dec 2006 18:05:40 +0100 wenzelm abbrevs: print original rhs;
Tue, 05 Dec 2006 00:30:38 +0100 wenzelm thm/prf: separate official name vs. additional tags;
Tue, 19 Sep 2006 23:15:38 +0200 wenzelm pretty_full_theory: suppress internal entities by default;
Thu, 27 Jul 2006 13:43:04 +0200 wenzelm removed obsolete pretty_thm_no_quote;
Wed, 26 Jul 2006 00:44:49 +0200 wenzelm moved pprint functions to Isar/proof_display.ML;
Tue, 11 Jul 2006 12:17:01 +0200 wenzelm Name.invent_list;
Wed, 07 Jun 2006 02:01:28 +0200 wenzelm renamed Type.(un)varifyT to Logic.(un)varifyT;
Tue, 23 May 2006 14:00:06 +0200 wenzelm made smlnj happy;
Tue, 23 May 2006 13:55:02 +0200 wenzelm pretty_full_theory: tuned output of definitions;
Mon, 22 May 2006 22:29:16 +0200 wenzelm pretty_full_theory: defs;
Tue, 16 May 2006 13:01:24 +0200 wenzelm more abstract interface to classes/arities;
Mon, 08 May 2006 17:40:07 +0200 wenzelm added raw_string_of_sort/typ/term;
Mon, 01 May 2006 17:05:09 +0200 wenzelm adapted arities;
Thu, 27 Apr 2006 15:06:35 +0200 wenzelm tuned basic list operators (flat, maps, map_filter);
Thu, 13 Apr 2006 12:00:58 +0200 wenzelm tuned comment;
Sat, 08 Apr 2006 22:51:19 +0200 wenzelm print_theory: print abbreviations nicely;
Tue, 21 Mar 2006 12:18:07 +0100 wenzelm subtract (op =);
Wed, 08 Feb 2006 17:15:27 +0100 wenzelm tuned;
Mon, 06 Feb 2006 20:59:03 +0100 wenzelm print_theory: const abbreviations;
Wed, 02 Nov 2005 14:46:57 +0100 wenzelm Consts.dest;
Thu, 27 Oct 2005 13:54:43 +0200 wenzelm consts: monomorphic;
Thu, 29 Sep 2005 00:58:57 +0200 wenzelm print_theory: discontinued final consts;
Sat, 17 Sep 2005 19:17:34 +0200 wenzelm pretty_thm_aux: ora masked by quick_and_dirty;
Sat, 17 Sep 2005 18:11:28 +0200 wenzelm pretty_thm_aux: aconv hyps;
Sat, 17 Sep 2005 12:18:03 +0200 wenzelm pretty_thm_aux: observe asms context;
Thu, 28 Jul 2005 15:19:54 +0200 wenzelm print_theory: const constraints;
Thu, 14 Jul 2005 19:28:28 +0200 wenzelm NameSpace.dest_table avoids duplicated extern;
Wed, 22 Jun 2005 19:41:19 +0200 wenzelm tuned;
less more (0) -100 -60 tip