| Sun, 07 May 2023 12:24:37 +0200 | wenzelm | minor performance tuning; | file | diff | annotate |
| Fri, 05 May 2023 11:47:38 +0200 | wenzelm | minor performance tuning; | file | diff | annotate |
| Fri, 05 May 2023 11:36:56 +0200 | wenzelm | tuned signature; | file | diff | annotate |
| Fri, 05 May 2023 11:29:27 +0200 | wenzelm | minor performance tuning; | file | diff | annotate |
| Wed, 03 May 2023 23:11:12 +0200 | wenzelm | tuned; | file | diff | annotate |
| Sun, 23 Apr 2023 21:31:00 +0200 | wenzelm | more operations for lexicographic ordering; | file | diff | annotate |
| Sun, 23 Apr 2023 19:57:40 +0200 | wenzelm | tuned; | file | diff | annotate |
| Fri, 14 Apr 2023 22:19:28 +0200 | wenzelm | tuned; | file | diff | annotate |
| Fri, 14 Apr 2023 22:08:16 +0200 | wenzelm | more operations; | file | diff | annotate |
| Fri, 14 Apr 2023 21:58:22 +0200 | wenzelm | tuned: more direct re-use; | file | diff | annotate |
| Fri, 14 Apr 2023 21:39:10 +0200 | wenzelm | more direct clone (see also change of exception in 8d8c70b41bab); | file | diff | annotate |
| Fri, 14 Apr 2023 21:34:51 +0200 | wenzelm | more operations, following Isabelle/ML conventions; | file | diff | annotate |
| Fri, 14 Apr 2023 20:42:17 +0200 | wenzelm | more operations, following Isabelle/ML conventions; | file | diff | annotate |
| Sun, 14 Aug 2022 11:20:10 +0200 | wenzelm | clarified signature: avoid confusing operation name (amending 8cf14d4ebec4); | file | diff | annotate |
| Fri, 05 Aug 2022 14:05:42 +0200 | wenzelm | more uniform exports: proper encoding of empty parents for Pure; | file | diff | annotate |
| Tue, 21 Jun 2022 22:17:11 +0200 | wenzelm | more scalable byte messages, notably for Scala functions in ML; | file | diff | annotate |
| Sat, 04 Sep 2021 22:05:35 +0200 | wenzelm | clarified signature; | file | diff | annotate |
| Fri, 18 Jun 2021 14:35:48 +0200 | wenzelm | tuned signature; | file | diff | annotate |
| Fri, 18 Jun 2021 12:12:28 +0200 | wenzelm | tuned signature; | file | diff | annotate |
| Fri, 18 Jun 2021 11:48:43 +0200 | wenzelm | tuned; | file | diff | annotate |
| Fri, 18 Jun 2021 11:32:32 +0200 | wenzelm | tuned signature (see 2d6a489adb01); | file | diff | annotate |
| Sat, 22 May 2021 13:35:25 +0200 | wenzelm | clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax; | file | diff | annotate |
| Mon, 12 Apr 2021 22:17:48 +0200 | wenzelm | unused; | file | diff | annotate |
| Mon, 01 Mar 2021 18:11:06 +0100 | wenzelm | clarified signature; | file | diff | annotate |
| Tue, 20 Aug 2019 11:01:05 +0200 | wenzelm | clarified signature; | file | diff | annotate |
| Sat, 03 Aug 2019 20:30:24 +0200 | wenzelm | clarified signature; | file | diff | annotate |
| Thu, 31 Jan 2019 16:32:41 +0100 | wenzelm | prefer tail-recursive version (despite 4b99b1214034); | file | diff | annotate |
| Fri, 14 Dec 2018 11:35:21 +0100 | wenzelm | tuned whitespace; | file | diff | annotate |
| Mon, 05 Nov 2018 15:00:22 +0100 | wenzelm | tuned (see map_index); | file | diff | annotate |
| Fri, 11 May 2018 19:59:05 +0200 | wenzelm | unused; | file | diff | annotate |