| Wed, 18 Oct 2023 22:09:25 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2023 16:29:24 +0200 |
wenzelm |
clarified signature: more concise simproc setup in ML;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2023 15:13:52 +0200 |
wenzelm |
clarified signature: more concise variations on implicit theory setup;
|
file |
diff |
annotate
|
| Tue, 17 Oct 2023 18:55:29 +0200 |
wenzelm |
support for "simproc_setup ... (passive)": allow to define simprocs in Isar that are not added to the simpset (yet);
|
file |
diff |
annotate
|
| Tue, 23 May 2023 18:46:15 +0200 |
wenzelm |
tuned signature: more position information;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2022 20:10:35 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 09 Apr 2021 21:07:11 +0200 |
wenzelm |
clarified signature: more detailed token positions for antiquotations;
|
file |
diff |
annotate
|
| Fri, 11 Oct 2019 21:51:10 +0200 |
wenzelm |
clarified standard_proof_of: prefer expand_proof over somewhat adhoc strip_thm_proof;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2019 20:09:25 +0200 |
wenzelm |
clarified global theory context;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2019 14:35:29 +0200 |
wenzelm |
clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction;
|
file |
diff |
annotate
|
| Mon, 03 Jun 2019 15:40:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 09 Mar 2019 23:57:07 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 09 Mar 2019 13:19:13 +0100 |
wenzelm |
clarified Toplevel.state: more explicit types;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 14:48:20 +0100 |
wenzelm |
clarified ML positions (see also 1a52baa70aed);
|
file |
diff |
annotate
|
| Wed, 31 Oct 2018 15:53:32 +0100 |
wenzelm |
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
|
file |
diff |
annotate
|
| Thu, 25 Oct 2018 21:29:08 +0200 |
wenzelm |
clarified ML position: proper markup for def/ref scopes (see also 162a4c2e97bc);
|
file |
diff |
annotate
|
| Mon, 27 Aug 2018 20:43:01 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2018 18:18:21 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 18:59:33 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Sat, 04 Feb 2017 21:15:11 +0100 |
wenzelm |
more uniform use of Reconstruct.clean_proof_of;
|
file |
diff |
annotate
|
| Sat, 06 Aug 2016 18:14:59 +0200 |
wenzelm |
more informative 'prf' and 'full_prf', based on HOL/Proofs/ex/XML_Data.thy;
|
file |
diff |
annotate
|
| 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
|