wenzelm [Fri, 05 May 2023 11:52:53 +0200] rev 77966
unused;
wenzelm [Fri, 05 May 2023 11:47:38 +0200] rev 77965
minor performance tuning;
wenzelm [Fri, 05 May 2023 11:36:56 +0200] rev 77964
tuned signature;
wenzelm [Fri, 05 May 2023 11:29:27 +0200] rev 77963
minor performance tuning;
wenzelm [Thu, 04 May 2023 23:30:59 +0200] rev 77962
revert pointless performance tuning fd5f4455e033: no measurable difference in HOL, HOL-Library, HOL-Analysis;
wenzelm [Thu, 04 May 2023 17:29:54 +0200] rev 77961
tuned;
wenzelm [Thu, 04 May 2023 11:42:04 +0200] rev 77960
more accurate treatment of traditional name space accesses (refining 948f5dc4d694, fcd85e04a948, 238307775d52);
more compact representation via Long_Name.chunks: avoid redundant string fragments from Long_Name.explode;
wenzelm [Wed, 03 May 2023 23:11:12 +0200] rev 77959
tuned;
wenzelm [Wed, 03 May 2023 11:34:47 +0200] rev 77958
proper treatment of restriction (for 'qualified');
tuned;
wenzelm [Tue, 02 May 2023 23:22:30 +0200] rev 77957
misc tuning;