Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Merged
  2. more on sublists
  3. tuned;
  4. more charts;
  5. uniform heap_scale; tuned;
  6. more plots from ml_statistics;
  7. simplified signature;
  8. tuned signature;
  9. more JFreeChart operations; tuned signature;
Changeset 65870:81574a7e7c38 by eberlm _eberlm@in.tum.de_:
Merged
Changeset 65869:a6ed757b8585 by eberlm _eberlm@in.tum.de_:
more on sublists
The file was modified src/HOL/Library/Sublist.thy (diff)
The file was modified src/HOL/Library/Sublist_Order.thy (diff)
Changeset 65868:65e132abab1e by wenzelm:
tuned;
The file was modified src/Pure/Admin/build_status.scala (diff)
Changeset 65867:53613acb76e7 by wenzelm:
more charts;
The file was modified src/Pure/Admin/build_status.scala (diff)
Changeset 65866:00e8b836d4db by wenzelm:
uniform heap_scale;<br>tuned;
The file was modified src/Pure/Admin/build_status.scala (diff)
The file was modified src/Pure/ML/ml_statistics.scala (diff)
Changeset 65865:177b90f33f40 by wenzelm:
more plots from ml_statistics;
The file was modified src/Pure/Admin/build_status.scala (diff)
Changeset 65864:1945fa8f0c39 by wenzelm:
simplified signature;
The file was modified src/Pure/ML/ml_statistics.scala (diff)
Changeset 65863:94fe5e82d101 by wenzelm:
tuned signature;
The file was modified src/Pure/Admin/build_status.scala (diff)
Changeset 65862:5441c51a2d38 by wenzelm:
more JFreeChart operations;<br>tuned signature;
The file was modified src/Pure/General/graphics_file.scala (diff)