| Sat, 09 Apr 2016 13:28:32 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2016 20:15:20 +0200 |
wenzelm |
eliminated unused simproc identifier;
|
file |
diff |
annotate
|
| Wed, 13 Jan 2016 16:55:56 +0100 |
wenzelm |
removed old 'defs' command;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 19:54:51 +0200 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Wed, 09 Sep 2015 20:57:21 +0200 |
wenzelm |
simplified simproc programming interfaces;
|
file |
diff |
annotate
|
| Wed, 02 Sep 2015 18:14:10 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 14:30:00 +0200 |
wenzelm |
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 15:28:06 +0200 |
wenzelm |
eliminated dead code;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 12:32:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 15:35:49 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 16:19:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 15:22:44 +0200 |
wenzelm |
discontinued pointless warnings: commands are only defined inside a theory context;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 14:18:32 +0200 |
wenzelm |
explicit error for Toplevel.proof_of;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 13:48:10 +0200 |
wenzelm |
clarified thy_deps;
|
file |
diff |
annotate
|
| Wed, 15 Apr 2015 19:08:37 +0200 |
wenzelm |
session graph with folded base theories, as in document preparation;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 12:51:25 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2015 19:56:51 +0200 |
wenzelm |
more uniform "verbose" option to print name space;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2014 20:42:45 +0100 |
wenzelm |
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
|
file |
diff |
annotate
|
| Wed, 31 Dec 2014 14:15:52 +0100 |
wenzelm |
for graph display, prefer graph data structure over list with dependencies;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2014 14:13:11 +0100 |
wenzelm |
more explict and generic field names
|
file |
diff |
annotate
|
| Wed, 31 Dec 2014 14:08:50 +0100 |
wenzelm |
uniform variable name for presentation graphs, to distinguish from values of type Graph.T
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 14:02:48 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 30 Nov 2014 12:24:56 +0100 |
wenzelm |
more abstract type Input.source;
|
file |
diff |
annotate
|
| Sat, 22 Nov 2014 13:38:15 +0100 |
wenzelm |
more careful ML source positions, for improved PIDE markup;
|
file |
diff |
annotate
|
| Wed, 12 Nov 2014 10:30:59 +0100 |
wenzelm |
more careful ML source positions, for improved PIDE markup;
|
file |
diff |
annotate
|
| Tue, 11 Nov 2014 20:11:38 +0100 |
wenzelm |
more careful ML source positions, for improved PIDE markup;
|
file |
diff |
annotate
|
| Tue, 11 Nov 2014 18:16:25 +0100 |
wenzelm |
more position information, e.g. relevant for errors in generated ML source;
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 16:59:40 +0100 |
wenzelm |
clarified legacy command;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 15:27:37 +0100 |
wenzelm |
uniform heading commands work in any context, even in theory header;
|
file |
diff |
annotate
|
| Sun, 07 Sep 2014 17:51:28 +0200 |
haftmann |
separated class_deps command into separate file
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 10:48:40 +0200 |
wenzelm |
tuned signature -- prefer self-contained user-space tool;
|
file |
diff |
annotate
|
| Fri, 25 Jul 2014 15:01:18 +0200 |
wenzelm |
old 'defs' is legacy --- slightly odd side-entry that bypasses regular Local_Theory.define interface;
|
file |
diff |
annotate
|
| Tue, 22 Jul 2014 14:03:00 +0200 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Mon, 05 May 2014 17:14:46 +0200 |
wenzelm |
clarified print operations for "terms" and "theorems";
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:35:39 +0200 |
wenzelm |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 17:56:13 +0100 |
wenzelm |
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 16:11:00 +0100 |
wenzelm |
separate tokenization and language context for SML: no symbols, no antiquotes;
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 13:18:10 +0100 |
wenzelm |
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 15:29:58 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 11:22:25 +0100 |
wenzelm |
more explicit treatment of verbose mode, which includes concealed entries;
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 10:14:42 +0100 |
wenzelm |
clarified print_local_facts;
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 22:57:50 +0100 |
wenzelm |
tuned signature -- clarified module name;
|
file |
diff |
annotate
|
| Sun, 09 Mar 2014 17:37:34 +0100 |
wenzelm |
more formal read_root;
|
file |
diff |
annotate
|
| Sun, 09 Mar 2014 17:08:31 +0100 |
wenzelm |
simplified / modernized hide commands: proper outer parsers and PIDE markup via check;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 20:35:50 +0200 |
wenzelm |
added Theory.setup convenience;
|
file |
diff |
annotate
|
| Sun, 07 Jul 2013 18:34:29 +0200 |
wenzelm |
discontinued command 'print_drafts';
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Sat, 30 Mar 2013 12:13:39 +0100 |
wenzelm |
item markup for Proof_Context.pretty_fact;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2013 16:16:22 +0100 |
wenzelm |
tuned -- less indirection;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2012 13:20:08 +0200 |
wenzelm |
more method position information, notably finished_pos after end of previous text;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 20:23:00 +0200 |
wenzelm |
more proof method text position information;
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 14:23:33 +0200 |
wenzelm |
tuned pretty_locale/print_locale, with more basic pretty_locale_deps based on that;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2012 15:40:41 +0200 |
wenzelm |
separate module Graph_Display;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2012 21:23:04 +0200 |
wenzelm |
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
|
file |
diff |
annotate
|
| Fri, 24 Aug 2012 12:35:39 +0200 |
wenzelm |
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 12:47:49 +0200 |
wenzelm |
clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
|
file |
diff |
annotate
|