Skip to content
Success

Changes

Summary

  1. merged
  2. tuned;
  3. merged
  4. code_target: create subdirectories for export_code file
  5. clarified signature: support "suppress" prefix as int, followed by list;
  6. minor performance tuning: more elementary operations;
  7. tuned signature;
  8. minor performance tuning: more elementary operations;
  9. tuned signature;
  10. more operations;
Changeset 77862:cba7246c2c32 by wenzelm:
merged
Changeset 77861:e1636a54dab0 by wenzelm:
tuned;
The file was modified src/Pure/General/long_name.ML (diff)
The file was modified src/Pure/General/name_space.ML (diff)
Changeset 77859:a11e25bdd247 by stuebinm _stuebinm@disroot.org_:
code_target: create subdirectories for export_code file
The file was modified src/Tools/Code/code_target.ML (diff)
Changeset 77858:30389d96d0d6 by wenzelm:
clarified signature: support "suppress" prefix as int, followed by list;
The file was modified src/Pure/General/long_name.ML (diff)
Changeset 77857:82041e01f383 by wenzelm:
minor performance tuning: more elementary operations;
The file was modified src/Pure/General/long_name.ML (diff)
Changeset 77856:e6de70b78117 by wenzelm:
tuned signature;
The file was modified src/Pure/General/long_name.ML (diff)
Changeset 77855:ff801186ff66 by wenzelm:
minor performance tuning: more elementary operations;
The file was modified src/Pure/General/long_name.ML (diff)
Changeset 77854:64533f3818a4 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)
The file was modified src/Pure/Tools/find_theorems.ML (diff)
Changeset 77853:5286dae99de3 by wenzelm:
more operations;
The file was modified src/Pure/General/vector.ML (diff)