| Wed, 23 Jul 2025 13:22:51 +0200 |
haftmann |
internal setting to identify pointless code drop: declarations
|
file |
diff |
annotate
|
| Sat, 12 Jul 2025 07:36:38 +0200 |
haftmann |
always use proper context when parsing constants
|
file |
diff |
annotate
|
| Thu, 26 Jun 2025 17:25:29 +0200 |
haftmann |
append (rather than prepend) code equations: the order within a theory is maintained in the resulting code
|
file |
diff |
annotate
|
| Thu, 26 Jun 2025 17:25:29 +0200 |
haftmann |
scope pending code equations to theories
|
file |
diff |
annotate
|
| Sat, 26 Apr 2025 21:33:48 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 25 Apr 2025 11:34:29 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 25 Apr 2025 11:22:25 +0200 |
wenzelm |
more scalable: discontinue odd shortcuts from 6b3739fee456, which produce bulky strings internally;
|
file |
diff |
annotate
|
| Sat, 26 Apr 2025 08:34:03 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 01 Dec 2024 14:01:47 +0100 |
wenzelm |
clarified signature: more operations;
|
file |
diff |
annotate
|
| Fri, 29 Nov 2024 17:40:15 +0100 |
wenzelm |
clarified signature: shorten common cases;
|
file |
diff |
annotate
|
| Sun, 31 Dec 2023 22:04:41 +0100 |
wenzelm |
minor performance tuning: proper Same.operation;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2023 13:39:40 +0100 |
wenzelm |
more general Logic.incr_indexes_operation;
|
file |
diff |
annotate
|
| Tue, 06 Jun 2023 21:02:37 +0200 |
wenzelm |
proper trim_context;
|
file |
diff |
annotate
|
| Tue, 06 Jun 2023 15:29:43 +0200 |
wenzelm |
proper exception positions;
|
file |
diff |
annotate
|
| Tue, 23 May 2023 18:46:15 +0200 |
wenzelm |
tuned signature: more position information;
|
file |
diff |
annotate
|
| Tue, 16 May 2023 19:52:50 +0200 |
wenzelm |
tuned: avoid duplication;
|
file |
diff |
annotate
|
| Mon, 15 May 2023 19:40:01 +0200 |
wenzelm |
more accurate Thm.trim_context / Thm.transfer;
|
file |
diff |
annotate
|
| Mon, 15 May 2023 15:14:19 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Mon, 15 May 2023 15:04:37 +0200 |
wenzelm |
clarified signature: avoid convoluted operations;
|
file |
diff |
annotate
|
| Tue, 02 May 2023 08:39:48 +0000 |
haftmann |
stripped unused functionality
|
file |
diff |
annotate
|
| Fri, 24 Mar 2023 18:30:17 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sat, 02 Apr 2022 17:03:35 +0000 |
haftmann |
pass constructor arity as part of case certficiate
|
file |
diff |
annotate
|
| Sun, 27 Mar 2022 19:27:52 +0000 |
haftmann |
prefer build combinator
|
file |
diff |
annotate
|
| Tue, 11 Jan 2022 06:47:47 +0000 |
haftmann |
more correct transfer
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 22:17:15 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 12 Jul 2021 11:41:02 +0000 |
haftmann |
proper local context
|
file |
diff |
annotate
|
| Fri, 17 Jul 2020 19:10:24 +0200 |
wenzelm |
clarified -- avoid non-standard extend/merge;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|