| Mon, 27 Jan 2025 12:13:37 +0100 |
wenzelm |
move theory "HOL-Library.Adhoc_Overloading" to Pure;
|
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, 30 Nov 2024 16:42:22 +0100 |
wenzelm |
clarified 'unbundle' polarity, according to algebraic group laws;
|
file |
diff |
annotate
|
| Sat, 05 Oct 2024 14:58:36 +0200 |
wenzelm |
first-class support for "unbundle no foobar_syntax" -- avoid redundant "bundle no_foobar_syntax" definitions;
|
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
|
| Sat, 20 May 2023 17:18:44 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 18 May 2023 17:21:29 +0200 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Sun, 15 Jan 2023 18:30:18 +0100 |
wenzelm |
isabelle update -u cite;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2023 21:33:49 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Sat, 10 Sep 2022 19:37:33 +0200 |
wenzelm |
more documentation of 'export_classpath' (session ROOT) and 'scala_build_generated_files' (Isar command);
|
file |
diff |
annotate
|
| Fri, 22 Jul 2022 16:41:15 +0200 |
wenzelm |
more documentation;
|
file |
diff |
annotate
|
| Wed, 09 Jun 2021 18:04:22 +0000 |
haftmann |
global interpretation into nested targets
|
file |
diff |
annotate
|
| Sun, 23 May 2021 19:59:37 +0200 |
wenzelm |
clarified index, more like formal @{element_ref};
|
file |
diff |
annotate
|
| Thu, 20 May 2021 22:02:19 +0200 |
wenzelm |
tuned index;
|
file |
diff |
annotate
|
| Thu, 03 Dec 2020 23:00:23 +0100 |
ballarin |
Highlight that 'intro_locales' and 'trace_locales' are useful debug features, plus minor clarifications.
|
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
|
| Mon, 08 Jun 2020 21:55:14 +0200 |
wenzelm |
clarified sessions;
|
file |
diff |
annotate
|
| Wed, 18 Mar 2020 17:29:20 +0100 |
wenzelm |
tuned documentation, based on hints by Pedro Sánchez Terraf;
|
file |
diff |
annotate
|
| Tue, 26 Nov 2019 08:09:44 +0100 |
ballarin |
Remove diagnostic command 'print_dependencies'.
|
file |
diff |
annotate
|
| Sat, 24 Aug 2019 12:03:00 +0200 |
ballarin |
Tracing of locale activation.
|
file |
diff |
annotate
|
| Sat, 17 Aug 2019 12:44:22 +0200 |
wenzelm |
added command 'thm_oracles';
|
file |
diff |
annotate
|
| Fri, 10 May 2019 11:20:02 +0200 |
wenzelm |
clarified documentation;
|
file |
diff |
annotate
|
| Fri, 10 May 2019 10:41:38 +0200 |
wenzelm |
more documentation;
|
file |
diff |
annotate
|
| Thu, 04 Apr 2019 22:18:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 04 Apr 2019 22:18:16 +0200 |
wenzelm |
documentation for generated files;
|
file |
diff |
annotate
|
| Sun, 24 Mar 2019 13:48:46 +0100 |
wenzelm |
documentation of document markers and re-interpreted command tags;
|
file |
diff |
annotate
|
| Thu, 14 Mar 2019 16:55:06 +0100 |
wenzelm |
more specific keyword kinds;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Wed, 19 Sep 2018 21:06:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 25 May 2018 23:11:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 25 May 2018 22:47:57 +0200 |
wenzelm |
added command 'ML_export';
|
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:16:32 +0100 |
wenzelm |
allow multiple entries of and_list (on both sides);
|
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
|
| Wed, 25 Oct 2017 13:47:53 +0200 |
wenzelm |
more documentation;
|
file |
diff |
annotate
|
| Mon, 02 Oct 2017 19:28:18 +0200 |
wenzelm |
added command 'external_file';
|
file |
diff |
annotate
|
| Mon, 03 Jul 2017 13:51:55 +0200 |
wenzelm |
added command 'alias' and 'type_alias';
|
file |
diff |
annotate
|
| Mon, 17 Apr 2017 15:08:21 +0200 |
wenzelm |
more uniform thy_deps (like class_deps), see also c48d536231fe;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2016 17:53:55 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 02 Aug 2016 17:39:38 +0200 |
wenzelm |
clarified: 'imports' is de-facto mandatory;
|
file |
diff |
annotate
|
| Tue, 02 Aug 2016 17:35:18 +0200 |
wenzelm |
support 'abbrevs' within theory header;
|
file |
diff |
annotate
|
| Wed, 20 Jul 2016 21:26:11 +0200 |
wenzelm |
clarified imports;
|
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
|
| Thu, 09 Jun 2016 17:14:13 +0200 |
wenzelm |
documentation;
|
file |
diff |
annotate
|
| Mon, 30 May 2016 14:15:44 +0200 |
wenzelm |
allow 'for' fixes for multi_specs;
|
file |
diff |
annotate
|
| Sun, 29 May 2016 15:40:25 +0200 |
wenzelm |
clarified check_open_spec / read_open_spec;
|
file |
diff |
annotate
|
| Sat, 28 May 2016 21:38:58 +0200 |
wenzelm |
clarified 'axiomatization';
|
file |
diff |
annotate
|
| Sun, 24 Apr 2016 21:31:14 +0200 |
wenzelm |
added Isar command 'define';
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 11:31:13 +0200 |
wenzelm |
clarified syntax;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 17:20:21 +0200 |
wenzelm |
updated documentation;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 23:58:48 +0200 |
wenzelm |
more uniform ML file commands;
|
file |
diff |
annotate
|
| Wed, 13 Jan 2016 21:44:26 +0100 |
wenzelm |
clarified example;
|
file |
diff |
annotate
|
| Wed, 13 Jan 2016 21:15:23 +0100 |
wenzelm |
updated section on "Overloaded constant definitions";
|
file |
diff |
annotate
|
| Sat, 19 Dec 2015 17:03:17 +0100 |
haftmann |
documentation on last state of the art concerning interpretation
|
file |
diff |
annotate
|
| Wed, 16 Dec 2015 16:31:36 +0100 |
wenzelm |
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
|
file |
diff |
annotate
|