| Wed, 20 Dec 2023 12:50:38 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 08 May 2023 11:09:18 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 05 May 2023 11:36:56 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 04 May 2023 23:30:59 +0200 |
wenzelm |
revert pointless performance tuning fd5f4455e033: no measurable difference in HOL, HOL-Library, HOL-Analysis;
|
file |
diff |
annotate
|
| Mon, 01 May 2023 13:09:53 +0200 |
wenzelm |
minor performance tuning: more compact, more sharing;
|
file |
diff |
annotate
|
| Mon, 01 May 2023 12:18:10 +0200 |
wenzelm |
potential performance tuning: more compact data structure, but less sharing;
|
file |
diff |
annotate
|
| Sun, 30 Apr 2023 21:49:39 +0200 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Wed, 26 Apr 2023 22:02:59 +0200 |
wenzelm |
performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
|
file |
diff |
annotate
|
| Wed, 26 Apr 2023 15:38:49 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 15 Apr 2023 22:26:22 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 15 Apr 2023 15:19:58 +0200 |
wenzelm |
clarified signature: support "suppress" prefix as int, followed by list;
|
file |
diff |
annotate
|
| Sat, 15 Apr 2023 14:44:45 +0200 |
wenzelm |
minor performance tuning: more elementary operations;
|
file |
diff |
annotate
|
| Sat, 15 Apr 2023 14:42:58 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 15 Apr 2023 14:14:30 +0200 |
wenzelm |
minor performance tuning: more elementary operations;
|
file |
diff |
annotate
|
| Sat, 15 Apr 2023 13:52:06 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 14 Apr 2023 21:34:51 +0200 |
wenzelm |
more operations, following Isabelle/ML conventions;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2023 23:53:12 +0200 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2023 23:16:18 +0200 |
wenzelm |
compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
|
file |
diff |
annotate
|
| Mon, 03 Apr 2017 14:29:44 +0200 |
wenzelm |
proper qualifier (again, see df4cd6e1fdfa);
|
file |
diff |
annotate
|
| Fri, 03 Apr 2015 18:36:19 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 10:35:43 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 30 Apr 2014 13:11:24 +0200 |
wenzelm |
support for long names in Scala;
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 12:51:14 +0100 |
wenzelm |
clarified completion ordering: prefer local names;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 10:04:26 +0100 |
wenzelm |
more direct Long_Name.qualification;
|
file |
diff |
annotate
|
| Sat, 22 Feb 2014 16:58:02 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 16:53:07 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|