| Fri, 25 Apr 2025 16:54:39 +0200 |
wenzelm |
clarified signature: more scalable output;
|
file |
diff |
annotate
|
| Fri, 25 Apr 2025 11:22:25 +0200 |
wenzelm |
more scalable: discontinue odd shortcuts from 6b3739fee456, which produce bulky strings internally;
|
file |
diff |
annotate
|
| Wed, 29 Jan 2025 14:43:14 +0100 |
wenzelm |
more accurate syntax: follow documentation in "isar-ref" (and command 'syntax_consts');
|
file |
diff |
annotate
|
| Mon, 27 Jan 2025 21:31:02 +0100 |
wenzelm |
clarified syntax;
|
file |
diff |
annotate
|
| Mon, 27 Jan 2025 12:13:37 +0100 |
wenzelm |
move theory "HOL-Library.Adhoc_Overloading" to Pure;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2024 23:48:45 +0100 |
wenzelm |
commands 'syntax_types' and 'syntax_consts' now work in a local theory context;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2024 21:47:20 +0100 |
wenzelm |
syntax translations now work in a local theory context;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2024 17:35:53 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 02 Dec 2024 11:22:44 +0100 |
wenzelm |
proper context for extern operation: observe local options;
|
file |
diff |
annotate
|
| Mon, 02 Dec 2024 11:08:36 +0100 |
wenzelm |
proper context for extern/check operation: observe local options like names_unique;
|
file |
diff |
annotate
|
| Tue, 15 Oct 2024 14:57:23 +0200 |
wenzelm |
backout somewhat pointless 5ea48342e0ae: no need to declare syntax consts for translations (e.g. constraints);
|
file |
diff |
annotate
|
| Fri, 11 Oct 2024 10:29:47 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 09 Oct 2024 13:06:55 +0200 |
wenzelm |
more syntax bundles;
|
file |
diff |
annotate
|
| Fri, 04 Oct 2024 13:29:33 +0200 |
wenzelm |
clarified syntax for opening bundles;
|
file |
diff |
annotate
|
| Wed, 02 Oct 2024 22:08:52 +0200 |
wenzelm |
provide 'open_bundle' command;
|
file |
diff |
annotate
|
| Sun, 29 Sep 2024 21:40:37 +0200 |
wenzelm |
more flexible command syntax;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2024 22:45:18 +0200 |
wenzelm |
clarified concrete syntax;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2024 20:45:54 +0200 |
wenzelm |
more concrete syntax and more checks;
|
file |
diff |
annotate
|
| Wed, 14 Aug 2024 21:23:22 +0200 |
wenzelm |
support for congprocs in the Simplifier, closely following Norbert Schirmer et-al, but with only one "simproc" name space and "simproc_setup" command / ML antiquotation;
|
file |
diff |
annotate
|
| Sun, 04 Aug 2024 16:56:28 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Sun, 04 Aug 2024 12:21:13 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Sat, 08 Jun 2024 16:26:47 +0200 |
wenzelm |
more accurate output of Thm_Name.T wrt. facts name space;
|
file |
diff |
annotate
|
| Fri, 07 Jun 2024 23:53:31 +0200 |
wenzelm |
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
|
file |
diff |
annotate
|
| Sat, 21 Oct 2023 21:19:02 +0200 |
wenzelm |
simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe);
|
file |
diff |
annotate
|
| Fri, 20 Oct 2023 11:03:09 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 19 Oct 2023 11:30:16 +0200 |
wenzelm |
clarified signature: Named_Target.setup works both for global and local theory;
|
file |
diff |
annotate
|
| 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
|