Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more robust CSV syntax, e.g. for "pull_date";
  2. merged
  3. more scalable generated files and code export, using Bytes.T;
  4. more operations;
  5. proper execution of Bytes.write; tuned;
  6. Avoid calculations where not necessary.
  7. Prefer existing horner sum combinator.
  8. Executable lexords.
  9. Less warnings.
Changeset 75606:0f7cb6cd08fe by wenzelm:
more robust CSV syntax, e.g. for "pull_date";
The file was modified src/Pure/General/csv.scala (diff)
Changeset 75605:2a40ca7454bc by wenzelm:
merged
Changeset 75604:39df30349778 by wenzelm:
more scalable generated files and code export, using Bytes.T;
The file was modified src/HOL/Library/code_test.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/narrowing_generators.ML (diff)
The file was modified src/Pure/General/file.ML (diff)
The file was modified src/Pure/Thy/export.ML (diff)
The file was modified src/Pure/Tools/generated_files.ML (diff)
The file was modified src/Tools/Code/code_printer.ML (diff)
The file was modified src/Tools/Code/code_runtime.ML (diff)
The file was modified src/Tools/Code/code_target.ML (diff)
Changeset 75603:fc8d64a578e4 by wenzelm:
more operations;
The file was modified src/Pure/General/bytes.ML (diff)
Changeset 75602:7a0d4c126f79 by wenzelm:
proper execution of Bytes.write;<br>tuned;
The file was modified src/Pure/General/bytes.ML (diff)
Changeset 75601:5ec227251b07 by haftmann:
Avoid calculations where not necessary.
The file was modified src/HOL/Library/Char_ord.thy (diff)
Changeset 75600:6de655ccac19 by haftmann:
Prefer existing horner sum combinator.
The file was modified NEWS (diff)
The file was modified src/HOL/Library/Char_ord.thy (diff)
Changeset 75599:36965f6b3530 by haftmann:
Executable lexords.
The file was modified src/HOL/List.thy (diff)
Changeset 75598:d078f8482155 by haftmann:
Less warnings.
The file was modified src/HOL/List.thy (diff)