| Mon, 13 May 2013 12:40:17 +0200 |
wenzelm |
retain goal display options when printing error messages, to avoid breakdown for huge goals;
|
file |
diff |
annotate
|
| Wed, 03 Apr 2013 13:58:00 +0200 |
wenzelm |
tuned output -- less bullets;
|
file |
diff |
annotate
|
| Sat, 30 Mar 2013 13:40:19 +0100 |
wenzelm |
more item markup;
|
file |
diff |
annotate
|
| Mon, 19 Nov 2012 20:23:47 +0100 |
wenzelm |
theorem status about oracles/futures is no longer printed by default;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 20:35:24 +0200 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 20:23:00 +0200 |
wenzelm |
more proof method text position information;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 15:14:12 +0200 |
wenzelm |
more informative errors for 'proof' and 'apply' steps;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 14:02:02 +0200 |
wenzelm |
further attempts to unify/simplify goal output;
|
file |
diff |
annotate
|
| Tue, 28 Feb 2012 16:43:32 +0100 |
wenzelm |
display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
|
file |
diff |
annotate
|
| Wed, 26 Oct 2011 22:51:06 +0200 |
wenzelm |
more robust ML pretty printing (cf. b6c527c64789);
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 16:46:58 +0200 |
wenzelm |
improved default context for ML toplevel pretty-printing;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 22:04:07 +0200 |
wenzelm |
less verbosity in batch mode -- spam reduction and notable performance improvement;
|
file |
diff |
annotate
|
| Thu, 12 May 2011 16:23:13 +0200 |
wenzelm |
proper configuration options Proof_Context.debug and Proof_Context.verbose;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 16:00:11 +0100 |
wenzelm |
tuned markup;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 21:44:52 +0200 |
wenzelm |
tuned markup;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 22:02:11 +0100 |
wenzelm |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 14:38:36 +0100 |
wenzelm |
print_theorems: suppress concealed (global) facts, unless "!" option is given;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:57:48 +0100 |
wenzelm |
modernized structure Proof_Display;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 16:52:16 +0200 |
wenzelm |
clarified pretty_goals, pretty_thm_aux: plain context;
|
file |
diff |
annotate
|
| 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.;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 21 Mar 2009 20:00:23 +0100 |
wenzelm |
removed obsolete pprint operations;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Fri, 12 Sep 2008 12:04:16 +0200 |
wenzelm |
more procise printing of fact names;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 22:20:16 +0200 |
wenzelm |
no pervasive bindings;
|
file |
diff |
annotate
|