Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more operations;
  2. clarified theory_sizeof1_data: count bytes, individually for each data entry;
  3. clarified operations for ML object sizes;
Changeset 77694:ea509b0bfc80 by wenzelm:
more operations;
The file was modified src/Pure/General/space.scala (diff)
Changeset 77693:068ff989c143 by wenzelm:
clarified theory_sizeof1_data: count bytes, individually for each data entry;
The file was modified src/Pure/context.ML (diff)
Changeset 77692:3e746e684f4b by wenzelm:
clarified operations for ML object sizes;
The file was modified NEWS (diff)
The file was modified src/Pure/ML/ml_heap.ML (diff)
The file was modified src/Pure/ML/ml_system.ML (diff)