Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
  2. tuned signature;
Changeset 77914:5aae99b191eb by wenzelm:
performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
The file was modified src/Pure/General/long_name.ML (diff)
Changeset 77913:019186a60c84 by wenzelm:
tuned signature;
The file was modified src/Pure/General/long_name.ML (diff)
The file was modified src/Pure/General/name_space.ML (diff)