src/Pure/Isar/proof_display.ML
Wed, 26 Oct 2011 22:51:06 +0200 wenzelm more robust ML pretty printing (cf. b6c527c64789);
Wed, 17 Aug 2011 16:46:58 +0200 wenzelm improved default context for ML toplevel pretty-printing;
Sat, 13 Aug 2011 22:04:07 +0200 wenzelm less verbosity in batch mode -- spam reduction and notable performance improvement;
Thu, 12 May 2011 16:23:13 +0200 wenzelm proper configuration options Proof_Context.debug and Proof_Context.verbose;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Fri, 14 Jan 2011 16:00:11 +0100 wenzelm tuned markup;
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
Thu, 09 Sep 2010 21:44:52 +0200 wenzelm tuned markup;
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Thu, 12 Nov 2009 22:02:11 +0100 wenzelm eliminated obsolete "internal" kind -- collapsed to unspecific "";
Sun, 08 Nov 2009 14:38:36 +0100 wenzelm print_theorems: suppress concealed (global) facts, unless "!" option is given;
Mon, 02 Nov 2009 20:57:48 +0100 wenzelm modernized structure Proof_Display;
Thu, 23 Jul 2009 16:52:16 +0200 wenzelm clarified pretty_goals, pretty_thm_aux: plain context;
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Thu, 26 Mar 2009 15:20:50 +0100 wenzelm pretty_rule/print_results: no thm status here -- it is potentially slow and mostly uninformative/confusing as long as proofs are still unfinished;
Sat, 21 Mar 2009 20:00:23 +0100 wenzelm removed obsolete pprint operations;
Sun, 08 Mar 2009 17:26:14 +0100 wenzelm moved basic algebra of long names from structure NameSpace to Long_Name;
Thu, 05 Mar 2009 12:08:00 +0100 wenzelm renamed NameSpace.base to NameSpace.base_name;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Fri, 12 Sep 2008 12:04:16 +0200 wenzelm more procise printing of fact names;
Tue, 02 Sep 2008 22:20:16 +0200 wenzelm no pervasive bindings;
Tue, 02 Sep 2008 18:01:24 +0200 wenzelm pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
Wed, 13 Aug 2008 20:57:31 +0200 wenzelm removed obsolete present_results;
Thu, 12 Jun 2008 16:41:58 +0200 wenzelm Facts.dest/export_static: content difference;
Sun, 18 May 2008 15:04:43 +0200 wenzelm pprint: proper global context via Syntax.init_pretty_global;
Wed, 16 Apr 2008 21:53:04 +0200 wenzelm pretty_theorems: use proper PureThy.facts_of;
Wed, 26 Mar 2008 22:40:07 +0100 wenzelm adapted to Context.thread_data interface;
Thu, 20 Mar 2008 16:04:30 +0100 wenzelm Facts.Named: include position;
Wed, 19 Mar 2008 22:27:57 +0100 wenzelm renamed datatype thmref to Facts.ref, tuned interfaces;
Tue, 09 Oct 2007 00:20:13 +0200 wenzelm generic Syntax.pretty/string_of operations;
Tue, 08 May 2007 17:40:20 +0200 wenzelm tuned ProofDisplay.pretty_full_theory;
Sat, 17 Feb 2007 17:19:59 +0100 aspinall pretty_full_theory: expose in signature.
Fri, 19 Jan 2007 22:08:02 +0100 wenzelm moved ML context stuff to from Context to ML_Context;
Fri, 19 Jan 2007 13:09:33 +0100 wenzelm adapted ML context operations;
Tue, 21 Nov 2006 18:07:33 +0100 wenzelm moved theorem kinds from PureThy to Thm;
Sat, 07 Oct 2006 01:31:17 +0200 wenzelm added pretty_consts (from specification.ML);
Tue, 19 Sep 2006 23:15:26 +0200 wenzelm 'print_theory': bang option for full verbosity;
Wed, 02 Aug 2006 22:27:05 +0200 wenzelm moved debug option to proof_display.ML (again);
Sat, 29 Jul 2006 00:51:36 +0200 wenzelm rename legacy_pretty_thm to pretty_thm_legacy;
Thu, 27 Jul 2006 13:43:13 +0200 wenzelm ProofContext.legacy_pretty_thm;
Wed, 26 Jul 2006 00:44:49 +0200 wenzelm moved pprint functions to Isar/proof_display.ML;
Thu, 27 Apr 2006 15:06:35 +0200 wenzelm tuned basic list operators (flat, maps, map_filter);
Thu, 13 Apr 2006 12:01:10 +0200 wenzelm added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
Fri, 27 Jan 2006 19:03:02 +0100 wenzelm moved theorem tags from Drule to PureThy;
Tue, 04 Oct 2005 19:01:37 +0200 wenzelm minor tweaks for Poplog/ML;
Tue, 13 Sep 2005 22:19:54 +0200 wenzelm Printing of Isar proof elements etc.
less more (0) tip