| Tue, 02 May 2023 19:49:17 +0200 | wenzelm | more standard name bindings (amending 5bf71b4da706): avoid odd full_name like "Orderings.class.Orderings.preorder.of_class.intro" with many redundant name space accesses; | file | diff | annotate |
| Wed, 09 Mar 2022 16:21:58 +0000 | paulson | A tiny further cleanup | file | diff | annotate |
| Wed, 09 Jun 2021 18:04:22 +0000 | haftmann | global interpretation into nested targets | file | diff | annotate |
| Wed, 02 Jun 2021 12:45:27 +0000 | haftmann | lexorders the locale way | file | diff | annotate |