| Wed, 29 Jan 2025 14:43:14 +0100 |
wenzelm |
more accurate syntax: follow documentation in "isar-ref" (and command 'syntax_consts');
|
changeset |
files
|
| Wed, 29 Jan 2025 11:53:49 +0100 |
wenzelm |
more robust: make double sure that buffer.getText() is valid (see also 2e7073976c25);
|
changeset |
files
|
| Tue, 28 Jan 2025 21:42:51 +0100 |
haftmann |
clarifed terminology
|
changeset |
files
|
| Tue, 28 Jan 2025 21:42:04 +0100 |
nipkow |
extracted the ^^ subtheory for modularity reasons
|
changeset |
files
|
| Tue, 28 Jan 2025 17:30:00 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Tue, 28 Jan 2025 14:53:36 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 28 Jan 2025 14:53:08 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 28 Jan 2025 13:42:40 +0100 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Tue, 28 Jan 2025 13:37:02 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 28 Jan 2025 13:35:08 +0100 |
wenzelm |
tuned names;
|
changeset |
files
|
| Tue, 28 Jan 2025 13:33:07 +0100 |
wenzelm |
minor performance tuning: avoid somewhat indirect filter / add_consts;
|
changeset |
files
|
| Tue, 28 Jan 2025 11:29:42 +0100 |
wenzelm |
clarified signature: more standard map_data;
|
changeset |
files
|
| Tue, 28 Jan 2025 11:20:53 +0100 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Tue, 28 Jan 2025 11:17:07 +0100 |
wenzelm |
clarified signature with minor performance tuning: avoid Context.proof_of with its Proof_Context.init_global;
|
changeset |
files
|
| Tue, 28 Jan 2025 11:05:45 +0100 |
wenzelm |
tuned names;
|
changeset |
files
|
| Tue, 28 Jan 2025 13:02:42 +0100 |
haftmann |
more explicit tests for non-PolyML SML platforms
|
changeset |
files
|
| Tue, 28 Jan 2025 07:17:30 +0100 |
haftmann |
typo
|
changeset |
files
|
| Mon, 27 Jan 2025 22:27:18 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 27 Jan 2025 21:31:11 +0100 |
wenzelm |
more NEWS;
|
changeset |
files
|
| Mon, 27 Jan 2025 21:31:02 +0100 |
wenzelm |
clarified syntax;
|
changeset |
files
|
| Mon, 27 Jan 2025 20:29:02 +0100 |
wenzelm |
support for "no" polarity of 'adhoc_overloading' vs. 'no_adhoc_overloading';
|
changeset |
files
|
| Mon, 27 Jan 2025 18:32:18 +0100 |
wenzelm |
more operations;
|
changeset |
files
|
| Mon, 27 Jan 2025 14:14:30 +0100 |
wenzelm |
clarified signature: proper ML interface to main command, without exposing too many internals;
|
changeset |
files
|
| Mon, 27 Jan 2025 12:52:19 +0100 |
wenzelm |
tuned signature: more explicit Type.raw_equiv;
|
changeset |
files
|
| Mon, 27 Jan 2025 12:24:51 +0100 |
wenzelm |
more liberal type equivalence, following thys/Transport/HOL_Basics/Adhoc_Overloading/Adhoc_Overloading.thy from AFP/e69d71bc07c4;
|
changeset |
files
|
| Mon, 27 Jan 2025 12:13:37 +0100 |
wenzelm |
move theory "HOL-Library.Adhoc_Overloading" to Pure;
|
changeset |
files
|
| Sun, 26 Jan 2025 22:45:57 +0100 |
wenzelm |
discontinue odd "-build" suffix altogether (see also f51b0b54b20b, bec95e287d26, 6b45a1568637);
|
changeset |
files
|
| Mon, 27 Jan 2025 13:13:30 +0100 |
haftmann |
more frugal exports
|
changeset |
files
|
| Mon, 27 Jan 2025 13:13:28 +0100 |
haftmann |
clarified scopes
|
changeset |
files
|
| Mon, 27 Jan 2025 07:39:49 +0100 |
haftmann |
more correct SML for SML/NJ
|
changeset |
files
|
| Mon, 27 Jan 2025 07:39:48 +0100 |
haftmann |
more explicit real operations
|
changeset |
files
|
| Sun, 26 Jan 2025 13:27:41 +0000 |
paulson |
merged
|
changeset |
files
|