Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned proofs;
  2. more symbols;
  3. more formal comments;
  4. more args;
  5. record active execution task and depend on it -- avoid new executions bumping into old ones;
  6. tuned -- more explicit types;
  7. less frequent consolidation: it requires a full Document.update and Document.start_execution;
Changeset 68358:e761afd35baa by wenzelm:
tuned proofs;
The file was modified src/HOL/HOLCF/Map_Functions.thy (diff)
Changeset 68357:6bf71e776226 by wenzelm:
more symbols;
The file was modified src/HOL/HOLCF/Domain.thy (diff)
Changeset 68356:46d5a9f428e1 by wenzelm:
more formal comments;
The file was modified src/HOL/Library/Extended_Real.thy (diff)
The file was modified src/HOL/Library/Lub_Glb.thy (diff)
Changeset 68355:67a4db47e4f6 by wenzelm:
more args;
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 68354:93d3c967802e by wenzelm:
record active execution task and depend on it -- avoid new executions bumping into old ones;
The file was modified src/Pure/Concurrent/task_queue.ML (diff)
The file was modified src/Pure/PIDE/document.ML (diff)
The file was modified src/Pure/PIDE/execution.ML (diff)
Changeset 68353:29cbe9e8ecde by wenzelm:
tuned -- more explicit types;
The file was modified src/Pure/PIDE/execution.ML (diff)
Changeset 68352:38272f9481c2 by wenzelm:
less frequent consolidation: it requires a full Document.update and Document.start_execution;
The file was modified etc/options (diff)