Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. support native PID for ML process;
  2. merged
  3. clarified theory data: more robust merge;
  4. proper import sessions;
  5. more thorough extend/merge (for Theory.join_theory);
  6. more thorough extend/merge (for Theory.join_theory);
  7. more thorough extend/merge (for Theory.join_theory);
  8. more thorough extend/merge, notably for master_dir across Theory.join_theory (e.g. for @{file} antiquotation);
  9. more robust: avoid potential problems with encoding of directory name;
  10. tuned grouping
  11. yet another alias
Changeset 72052:912f13865596 by wenzelm:
support native PID for ML process;
The file was addedsrc/Pure/ML/ml_pid.ML
The file was modified src/Pure/ROOT.ML (diff)
Changeset 72051:438adb97d82c by wenzelm:
merged
Changeset 72050:d4de7e4754d2 by wenzelm:
clarified theory data: more robust merge;
The file was modified src/Pure/Tools/generated_files.ML (diff)
Changeset 72049:18d35be9493f by wenzelm:
proper import sessions;
The file was modified src/HOL/ROOT (diff)
Changeset 72048:d3b8c8b2d1fc by wenzelm:
more thorough extend/merge (for Theory.join_theory);
The file was modified src/Pure/more_thm.ML (diff)
Changeset 72047:b9e9ff3a1e1c by wenzelm:
more thorough extend/merge (for Theory.join_theory);
The file was modified src/Pure/Thy/present.ML (diff)
Changeset 72046:c386d1b77762 by wenzelm:
more thorough extend/merge (for Theory.join_theory);
The file was modified src/Pure/Tools/generated_files.ML (diff)
Changeset 72045:2c7cfd2f9b6c by wenzelm:
more thorough extend/merge, notably for master_dir across Theory.join_theory (e.g. for @{file} antiquotation);
The file was modified src/Pure/PIDE/resources.ML (diff)
Changeset 72044:efd169aed4dc by wenzelm:
more robust: avoid potential problems with encoding of directory name;
The file was modified src/Pure/ML/ml_statistics.scala (diff)
Changeset 72043:b8bcdb884651 by haftmann:
tuned grouping
The file was modified src/HOL/Word/Word.thy (diff)
Changeset 72042:587d4681240c by haftmann:
yet another alias
The file was modified NEWS (diff)
The file was modified src/HOL/Word/Bits_Int.thy (diff)
The file was modified src/HOL/Word/Word.thy (diff)