Skip to content
Failed

Changes

Summary

  1. tuned;
  2. experimental computations: use arbitrary generated code for RHSs, not just constants
  3. tuned documentation
Changeset 64941:730bc1bcf27c by wenzelm:
tuned;
The file was modified src/Pure/Admin/build_docker.scala (diff)
Changeset 64940:19ca3644ec46 by haftmann:
experimental computations: use arbitrary generated code for RHSs, not just constants
The file was modified src/Tools/Code/code_runtime.ML (diff)
Changeset 64939:c8626f7fae06 by traytel:
tuned documentation
The file was modified src/Doc/Datatypes/Datatypes.thy (diff)