| 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
|
| 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
|
| Sun, 08 Oct 2023 19:05:35 +0200 |
wenzelm |
discontinue obsolete "Interrupt" constructor (NB: catch-all pattern produces ML compiler error);
|
file |
diff |
annotate
|
| Thu, 28 Sep 2023 20:07:30 +0200 |
wenzelm |
explicitly reject 'handle' with catch-all patterns;
|
file |
diff |
annotate
|
| Sun, 13 Aug 2023 19:27:58 +0200 |
wenzelm |
clarified command arguments: optionally restrict to given theories (from theory loader);
|
file |
diff |
annotate
|
| Sun, 13 Aug 2023 17:50:31 +0200 |
wenzelm |
added Isar command 'print_context_tracing';
|
file |
diff |
annotate
|
| Thu, 05 Jan 2023 21:33:49 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2022 11:25:49 +0200 |
wenzelm |
clarified message channel for 'print_state' (NB: the command was originally for TTY or Proof General);
|
file |
diff |
annotate
|
| Fri, 22 Jul 2022 15:28:56 +0200 |
wenzelm |
removed obsolete commands;
|
file |
diff |
annotate
|
| Fri, 22 Jul 2022 15:15:26 +0200 |
wenzelm |
command 'scala_build_generated_files' with proper management of source dependencies;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2022 15:42:57 +0200 |
wenzelm |
support for classpath artifacts within session structure:
|
file |
diff |
annotate
|
| Fri, 08 Jul 2022 22:29:26 +0200 |
wenzelm |
support for Isabelle/Scala/Java modules in Isabelle/ML;
|
file |
diff |
annotate
|
| Mon, 06 Dec 2021 15:34:54 +0100 |
wenzelm |
discontinued old-style {* verbatim *} tokens;
|
file |
diff |
annotate
|
| Thu, 28 Oct 2021 12:09:58 +0200 |
wenzelm |
clarified keywords: major take precedence for commands, but not used for antiquotations;
|
file |
diff |
annotate
|
| Sun, 26 Sep 2021 18:49:55 +0200 |
wenzelm |
improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
|
file |
diff |
annotate
|
| Tue, 21 Sep 2021 12:08:41 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2021 23:15:02 +0200 |
wenzelm |
localized command 'syntax' and 'no_syntax';
|
file |
diff |
annotate
|
| Mon, 20 Sep 2021 20:22:32 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2021 14:24:57 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2021 12:54:28 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 26 May 2021 18:07:49 +0200 |
wenzelm |
more robust syntax;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2021 13:39:06 +0100 |
wenzelm |
more checks;
|
file |
diff |
annotate
|
| Mon, 07 Dec 2020 16:09:06 +0100 |
wenzelm |
more accurate markup (refining 1c59b555ac4a);
|
file |
diff |
annotate
|
| Sun, 06 Dec 2020 20:49:44 +0100 |
wenzelm |
more accurate syntax, following Sessions.parse_roots in Scala;
|
file |
diff |
annotate
|
| Sun, 06 Dec 2020 16:27:37 +0100 |
wenzelm |
PIDE support for session ROOTS;
|
file |
diff |
annotate
|
| Sat, 05 Dec 2020 12:14:40 +0100 |
wenzelm |
support for PIDE markup for auxiliary files ("blobs");
|
file |
diff |
annotate
|
| Fri, 27 Nov 2020 23:51:37 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 27 Nov 2020 21:59:23 +0100 |
wenzelm |
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
|
file |
diff |
annotate
|
| Fri, 27 Nov 2020 06:48:35 +0000 |
haftmann |
refined syntax for bundle mixins for locale and class specifications
|
file |
diff |
annotate
|
| Sun, 01 Nov 2020 16:54:49 +0100 |
haftmann |
bundle mixins for locale and class specifications
|
file |
diff |
annotate
|
| Mon, 12 Oct 2020 07:25:38 +0000 |
haftmann |
dedicated module for toplevel target handling
|
file |
diff |
annotate
|
| Sat, 10 Oct 2020 18:43:09 +0000 |
haftmann |
consolidated terminology
|
file |
diff |
annotate
|
| Mon, 02 Mar 2020 14:58:37 +0000 |
haftmann |
infrastructure for extraction of equations x = t from premises beneath meta-all
|
file |
diff |
annotate
|
| Tue, 26 Nov 2019 08:09:44 +0100 |
ballarin |
Remove diagnostic command 'print_dependencies'.
|
file |
diff |
annotate
|
| Fri, 23 Aug 2019 14:32:51 +0200 |
wenzelm |
clarified 'thm_deps' command;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2019 19:04:03 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2019 12:44:22 +0200 |
wenzelm |
added command 'thm_oracles';
|
file |
diff |
annotate
|
| Sun, 28 Apr 2019 13:09:15 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 17 Apr 2019 16:57:06 +0000 |
haftmann |
backed out experimental b67bab2b132c, which slipped in accidentally
|
file |
diff |
annotate
|
| Tue, 16 Apr 2019 19:50:30 +0000 |
haftmann |
hierarchically inclusive named theorem collections
|
file |
diff |
annotate
|
| Sat, 13 Apr 2019 13:30:02 +0200 |
wenzelm |
more abbrevs;
|
file |
diff |
annotate
|
| Thu, 04 Apr 2019 22:17:37 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 04 Apr 2019 20:45:55 +0200 |
wenzelm |
type Path.binding may be empty: check later via proper_binding;
|
file |
diff |
annotate
|