| 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
|
| 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
|
| Thu, 04 Apr 2019 16:47:09 +0200 |
wenzelm |
clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
|
file |
diff |
annotate
|
| Thu, 04 Apr 2019 14:30:58 +0200 |
wenzelm |
added command 'compile_generated_files';
|
file |
diff |
annotate
|
| Wed, 03 Apr 2019 21:50:00 +0200 |
wenzelm |
clarified signature: more explicit operations for corresponding Isar commands;
|
file |
diff |
annotate
|
| Thu, 28 Mar 2019 21:24:55 +0100 |
wenzelm |
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
|
file |
diff |
annotate
|
| Thu, 14 Mar 2019 16:55:06 +0100 |
wenzelm |
more specific keyword kinds;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 21:12:29 +0100 |
wenzelm |
document markers are formal comments, and may thus occur anywhere in the command-span;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 00:21:34 +0100 |
wenzelm |
added semantic document markers;
|
file |
diff |
annotate
|
| Tue, 15 Jan 2019 20:03:53 +0100 |
wenzelm |
added command 'export_generated_files';
|
file |
diff |
annotate
|
| Thu, 20 Dec 2018 12:40:24 +0000 |
haftmann |
disregard historic keyword
|
file |
diff |
annotate
|
| Sat, 01 Dec 2018 16:11:59 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 30 Nov 2018 23:43:10 +0100 |
wenzelm |
more general command 'generate_file' for registered file types, notably Haskell;
|
file |
diff |
annotate
|
| Tue, 27 Nov 2018 21:07:39 +0100 |
wenzelm |
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 13:42:36 +0100 |
wenzelm |
more standard Resources.provide_parse_files: avoid duplicate markup reports;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 19:53:45 +0200 |
wenzelm |
tuned signature: prefer value-oriented pretty-printing;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 19:34:14 +0200 |
wenzelm |
tuned signature: prefer value-oriented pretty-printing;
|
file |
diff |
annotate
|
| Sun, 02 Sep 2018 14:14:43 +0200 |
wenzelm |
no reset_proof for notepad: begin/end structure takes precedence over goal/proof structure;
|
file |
diff |
annotate
|
| Tue, 28 Aug 2018 11:22:04 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 28 Aug 2018 11:13:33 +0200 |
wenzelm |
clarified ML_environment: ML_write_global requires "Isabelle";
|
file |
diff |
annotate
|
| Mon, 27 Aug 2018 17:30:13 +0200 |
wenzelm |
clarified environment: allow "read>write" specification;
|
file |
diff |
annotate
|
| Mon, 27 Aug 2018 14:42:24 +0200 |
wenzelm |
support named ML environments, notably "Isabelle", "SML";
|
file |
diff |
annotate
|
| Sun, 26 Aug 2018 17:28:38 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 26 Jun 2018 14:01:46 +0200 |
wenzelm |
clarified default tag;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2018 14:49:21 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 25 May 2018 22:47:57 +0200 |
wenzelm |
added command 'ML_export';
|
file |
diff |
annotate
|
| Tue, 06 Mar 2018 22:59:00 +0100 |
ballarin |
Drop rewrite rule arguments of sublocale and interpretation implementations.
|
file |
diff |
annotate
|
| Sun, 04 Mar 2018 12:22:48 +0100 |
ballarin |
Drop rewrites after defines in interpretations.
|
file |
diff |
annotate
|
| Fri, 02 Mar 2018 14:19:25 +0100 |
ballarin |
Proper rewrite morphisms in locale instances.
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 19:30:55 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 19:28:05 +0100 |
ballarin |
Experimental support for rewrite morphisms in locale instances.
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 11:27:52 +0100 |
wenzelm |
discontinued old form of marginal comments;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2018 15:40:12 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 28 Dec 2017 12:07:52 +0100 |
wenzelm |
prefer existing Resources.check_path;
|
file |
diff |
annotate
|
| Thu, 28 Dec 2017 11:49:54 +0100 |
wenzelm |
added command 'bibtex_file' (for PIDE interaction only);
|
file |
diff |
annotate
|
| Fri, 22 Dec 2017 18:32:59 +0100 |
wenzelm |
discontinued 'display_drafts' command;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 18:59:33 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Sun, 03 Dec 2017 13:22:09 +0100 |
wenzelm |
discontinued old 'def' command;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2017 10:27:56 +0100 |
wenzelm |
clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2017 17:34:32 +0100 |
wenzelm |
formal dependency on "poly" executable;
|
file |
diff |
annotate
|
| Sun, 05 Nov 2017 17:45:17 +0100 |
wenzelm |
more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
|
file |
diff |
annotate
|
| Mon, 02 Oct 2017 19:28:18 +0200 |
wenzelm |
added command 'external_file';
|
file |
diff |
annotate
|
| Sun, 02 Jul 2017 20:13:38 +0200 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
file |
diff |
annotate
|
| Mon, 03 Jul 2017 13:51:55 +0200 |
wenzelm |
added command 'alias' and 'type_alias';
|
file |
diff |
annotate
|
| Mon, 26 Jun 2017 11:07:48 +0200 |
wenzelm |
clarified indentation;
|
file |
diff |
annotate
|
| Wed, 28 Dec 2016 10:39:50 +0100 |
wenzelm |
more uniform treatment of "bad" like other messages (with serial number);
|
file |
diff |
annotate
|
| Sun, 18 Dec 2016 12:34:31 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2016 14:37:38 +0200 |
wenzelm |
discontinued global etc/abbrevs;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2016 13:26:14 +0200 |
wenzelm |
strictly sequential abbrevs;
|
file |
diff |
annotate
|
| Tue, 02 Aug 2016 17:35:18 +0200 |
wenzelm |
support 'abbrevs' within theory header;
|
file |
diff |
annotate
|
| Sat, 16 Jul 2016 00:38:33 +0200 |
wenzelm |
information about proof outline with cases (sendback);
|
file |
diff |
annotate
|
| Fri, 15 Jul 2016 23:46:28 +0200 |
wenzelm |
singleton result for 'proof' command (without backtracking), e.g. relevant for well-defined output;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2016 20:58:00 +0200 |
wenzelm |
clarified indentation;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2016 16:36:29 +0200 |
wenzelm |
explicit kind "before_command";
|
file |
diff |
annotate
|
| Mon, 11 Jul 2016 10:43:54 +0200 |
wenzelm |
more indentation for quasi_command keywords;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2016 17:35:45 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 11 Jun 2016 16:41:11 +0200 |
wenzelm |
clarified syntax;
|
file |
diff |
annotate
|
| Fri, 10 Jun 2016 22:47:25 +0200 |
wenzelm |
added command 'unbundle';
|
file |
diff |
annotate
|
| Fri, 10 Jun 2016 12:45:34 +0200 |
wenzelm |
prefer hybrid 'bundle' command;
|
file |
diff |
annotate
|