Summary
- tuned;
- experimental computations: use arbitrary generated code for RHSs, not just constants
- tuned documentation
The file was modified | src/Pure/Admin/build_docker.scala (diff) |
The file was modified | src/Tools/Code/code_runtime.ML (diff) |
The file was modified | src/Doc/Datatypes/Datatypes.thy (diff) |