wenzelm [Mon, 01 May 2023 22:47:51 +0200] rev 77947
clarified extern vs. alias/hide: output alternative names, if possible;
minor performance tuning: no storage of accesses', produce Long_Name.chunks on the spot;
wenzelm [Mon, 01 May 2023 22:19:01 +0200] rev 77946
tuned;
wenzelm [Mon, 01 May 2023 13:09:53 +0200] rev 77945
minor performance tuning: more compact, more sharing;
wenzelm [Mon, 01 May 2023 12:18:10 +0200] rev 77944
potential performance tuning: more compact data structure, but less sharing;
paulson <lp15@cam.ac.uk> [Sun, 07 May 2023 14:52:53 +0100] rev 77943
Importation of additional lemmas from metric.ml
paulson <lp15@cam.ac.uk> [Sat, 06 May 2023 12:42:10 +0100] rev 77942
fixes esp to theory presentation
paulson <lp15@cam.ac.uk> [Sat, 06 May 2023 11:10:23 +0100] rev 77941
new material ported from HOL Light's metric.ml