| Mon, 23 Jun 2025 14:44:59 +0200 |
wenzelm |
re-use cache from Main_Plugin.start;
|
changeset |
files
|
| Mon, 23 Jun 2025 14:42:40 +0200 |
wenzelm |
clarified signature, following c3793899b880;
|
changeset |
files
|
| Mon, 23 Jun 2025 14:10:59 +0200 |
wenzelm |
more robust: assertion holds, because session.finished_theories provides Snapshot from Document.State.end_theory;
|
changeset |
files
|
| Mon, 23 Jun 2025 13:55:09 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Mon, 23 Jun 2025 13:41:56 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Mon, 23 Jun 2025 13:41:18 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Mon, 23 Jun 2025 12:42:53 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 25 Jun 2025 16:16:26 +0200 |
nipkow |
added lemmas
|
changeset |
files
|
| Wed, 25 Jun 2025 14:16:30 +0200 |
nipkow |
added lemmas
|
changeset |
files
|
| Thu, 19 Jun 2025 17:15:40 +0200 |
haftmann |
treat map_filter similar to list_all, list_ex, list_ex1
|
changeset |
files
|
| Tue, 17 Jun 2025 14:11:40 +0200 |
nipkow |
reinstated intersection of lists as inter_list_set
|
changeset |
files
|
| Tue, 17 Jun 2025 06:29:55 +0200 |
nipkow |
merged
|
changeset |
files
|
| Tue, 17 Jun 2025 06:28:24 +0200 |
nipkow |
defined mset in terms of its list-versin count_list instead of the ugly length of filter.
|
changeset |
files
|
| Mon, 16 Jun 2025 15:25:38 +0200 |
haftmann |
more explicit theorem names for list quantifiers
|
changeset |
files
|
| Mon, 16 Jun 2025 12:19:23 +0200 |
wenzelm |
support for explicit ML platform identifier;
|
changeset |
files
|
| Mon, 16 Jun 2025 12:18:26 +0200 |
wenzelm |
more robust;
|
changeset |
files
|
| Mon, 16 Jun 2025 11:40:35 +0200 |
wenzelm |
proper SSH operation (amending 956ecf2c07a0);
|
changeset |
files
|
| Mon, 16 Jun 2025 11:38:14 +0200 |
wenzelm |
more robust;
|
changeset |
files
|
| Mon, 16 Jun 2025 11:35:54 +0200 |
wenzelm |
tuned errors;
|
changeset |
files
|
| Mon, 16 Jun 2025 11:00:04 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 15 Jun 2025 23:09:43 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Sun, 15 Jun 2025 23:03:12 +0200 |
wenzelm |
more NEWS;
|
changeset |
files
|
| Sun, 15 Jun 2025 22:55:30 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sun, 15 Jun 2025 22:46:45 +0200 |
wenzelm |
more flexible ML_Settings in Isabelle/Scala, depending on system options and some default settings;
|
changeset |
files
|
| Sun, 15 Jun 2025 22:14:38 +0200 |
wenzelm |
support dynamic usage_text, after some options have been processed already;
|
changeset |
files
|
| Sun, 15 Jun 2025 15:19:03 +0200 |
wenzelm |
clarified signature: more modular, avoid adhoc mixins;
|
changeset |
files
|
| Sun, 15 Jun 2025 13:40:03 +0200 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
| Sun, 15 Jun 2025 13:13:37 +0200 |
wenzelm |
clarified signature: more explicit types;
|
changeset |
files
|
| Sat, 14 Jun 2025 22:35:48 +0200 |
wenzelm |
proper support for old versions before 0e41f26a0250;
|
changeset |
files
|
| Sat, 14 Jun 2025 22:20:57 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Sat, 14 Jun 2025 22:19:58 +0200 |
wenzelm |
proper Java command-line for desktop application (amending a3e7732b0393);
|
changeset |
files
|
| Sat, 14 Jun 2025 21:50:44 +0200 |
wenzelm |
more robust: inspect true ML environment instead of reconstructing it externally;
|
changeset |
files
|
| Sat, 14 Jun 2025 21:19:37 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 14 Jun 2025 21:07:09 +0200 |
wenzelm |
discontinue unused parameter (better done as system option);
|
changeset |
files
|
| Sat, 14 Jun 2025 17:10:18 +0200 |
wenzelm |
discontinued ML_IDENTIFIER settings variable;
|
changeset |
files
|
| Sat, 14 Jun 2025 14:37:34 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Sat, 14 Jun 2025 14:34:11 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 14 Jun 2025 14:31:54 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 14 Jun 2025 13:47:55 +0200 |
nipkow |
removed pointless leftovers
|
changeset |
files
|
| Sat, 14 Jun 2025 11:45:56 +0200 |
nipkow |
more minus_list lemmas (incl code via fold instead of foldr)
|
changeset |
files
|
| Sat, 14 Jun 2025 00:22:10 +0200 |
nipkow |
make canonical homomorphism [simp]
|
changeset |
files
|
| Fri, 13 Jun 2025 20:59:51 +0200 |
nipkow |
the canonical homomorphism should be [simp]
|
changeset |
files
|
| Fri, 13 Jun 2025 17:16:53 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 13 Jun 2025 17:16:38 +0200 |
nipkow |
added minus functions on lists
|
changeset |
files
|
| Fri, 13 Jun 2025 15:18:16 +0200 |
wenzelm |
more robust GUI setup via Java, instead of shell script;
|
changeset |
files
|
| Thu, 12 Jun 2025 16:54:28 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 12 Jun 2025 12:59:17 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Thu, 12 Jun 2025 12:53:54 +0200 |
wenzelm |
avoid legacy infixes;
|
changeset |
files
|
| Thu, 12 Jun 2025 12:44:47 +0200 |
wenzelm |
discontinue old infixes;
|
changeset |
files
|
| Thu, 12 Jun 2025 10:38:02 +0200 |
haftmann |
eliminated transitional lemma
|
changeset |
files
|
| Thu, 12 Jun 2025 10:37:57 +0200 |
haftmann |
tuned whitespace
|
changeset |
files
|
| Thu, 12 Jun 2025 08:03:05 +0200 |
haftmann |
reorganized more code-only operations
|
changeset |
files
|
| Mon, 09 Jun 2025 22:14:38 +0200 |
haftmann |
more qualified auxiliary operations
|
changeset |
files
|
| Fri, 06 Jun 2025 18:36:29 +0100 |
paulson |
Sylvestre's correction to ex_least_nat_le and other tidying
|
changeset |
files
|
| Fri, 06 Jun 2025 16:18:44 +0100 |
paulson |
New lemmas for floor/ceiling/round, plus tidying
|
changeset |
files
|
| Thu, 05 Jun 2025 15:18:27 +0000 |
haftmann |
prefer already existing operation to calculate minimum
|
changeset |
files
|
| Wed, 04 Jun 2025 19:43:13 +0000 |
haftmann |
some more lemmas
|
changeset |
files
|
| Wed, 04 Jun 2025 19:43:13 +0000 |
haftmann |
tuned syntax
|
changeset |
files
|
| Wed, 04 Jun 2025 09:52:40 +0200 |
nipkow |
latex error
|
changeset |
files
|
| Tue, 03 Jun 2025 15:18:54 +0200 |
Manuel Eberl |
HOL: minor additions regarding linear algebra
|
changeset |
files
|