Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. less ambitious parallelism, notably for threads=2;
  2. more informative error, notably for missing executable;
  3. tuned signature;
  4. clarified future scheduling parameters, with support for parallel_limit;
  5. record total number of tasks;
  6. merged
  7. more infinite product theorems
  8. proper merge of items without term index (amending b969263fcf02);
  9. announce sorted changes
Changeset 68133:f6a22490cca8 by wenzelm:
less ambitious parallelism, notably for threads=2;
The file was modified src/HOL/ROOT (diff)
Changeset 68132:2a5ae592eafb by wenzelm:
more informative error, notably for missing executable;
The file was modified src/Pure/Thy/present.scala (diff)
Changeset 68131:62a3294edda3 by wenzelm:
tuned signature;
The file was modified src/Pure/General/exn.scala (diff)
The file was modified src/Pure/ROOT.scala (diff)
Changeset 68130:6fb85346cb79 by wenzelm:
clarified future scheduling parameters, with support for parallel_limit;
The file was modified etc/options (diff)
The file was modified src/Pure/Concurrent/future.ML (diff)
The file was modified src/Pure/Concurrent/lazy.ML (diff)
The file was modified src/Pure/Concurrent/multithreading.ML (diff)
The file was modified src/Pure/Concurrent/par_list.ML (diff)
The file was modified src/Pure/Isar/proof.ML (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)
The file was modified src/Pure/ML/ml_compiler.ML (diff)
The file was modified src/Pure/PIDE/command.ML (diff)
The file was modified src/Pure/PIDE/execution.ML (diff)
The file was modified src/Pure/Thy/thy_info.ML (diff)
The file was modified src/Pure/goal.ML (diff)
The file was modified src/Pure/par_tactical.ML (diff)
Changeset 68129:b73678836f8e by wenzelm:
record total number of tasks;
The file was modified src/Pure/Concurrent/future.ML (diff)
The file was modified src/Pure/Concurrent/task_queue.ML (diff)
The file was modified src/Pure/ML/ml_statistics.scala (diff)
Changeset 68128:4646124e683e by paulson:
merged
Changeset 68127:137d5d0112bb by paulson _lp15@cam.ac.uk_:
more infinite product theorems
The file was modified src/HOL/Analysis/Infinite_Products.thy (diff)
The file was modified src/HOL/Series.thy (diff)
Changeset 68126:5da8b97d9183 by wenzelm:
proper merge of items without term index (amending b969263fcf02);
The file was modified src/Pure/item_net.ML (diff)
Changeset 68125:2e5b737810a6 by nipkow:
announce sorted changes
The file was modified NEWS (diff)
The file was modified src/HOL/Data_Structures/Sorted_Less.thy (diff)
The file was modified src/HOL/List.thy (diff)