Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. prefer physical processors (see also 4b014e6c1dfe and 26a43785590b);
  3. more robust: avoid occasional problems reading this special file (e.g. SSH.Local or "lxcisa0");
  4. more robust default;
  5. more accurate, notably on lxbroy10 and vmnipkow9;
  6. clarified num_processors: follow Poly/ML (with its inaccuracies);
  7. clarified modules, following Isabelle/ML;
  8. clarified signature;
  9. tuned comments;
  10. merged
  11. the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses
  12. merged
  13. A few lemmas brought in from AFP entries
  14. merged
  15. made destructor-view tactic more robust (by Jan van Brügge)
Changeset 79609:71731d28b86d by wenzelm:
merged
Changeset 79608:f1df99019b50 by wenzelm:
prefer physical processors (see also 4b014e6c1dfe and 26a43785590b);
The file was modified src/Pure/System/host.scala (diff)
Changeset 79607:118504de9d0d by wenzelm:
more robust: avoid occasional problems reading this special file (e.g. SSH.Local or "lxcisa0");
The file was modified src/Pure/Concurrent/multithreading.scala (diff)
Changeset 79606:d1f060886590 by wenzelm:
more robust default;
The file was modified src/Pure/Concurrent/multithreading.scala (diff)
Changeset 79605:83627a092fbf by wenzelm:
more accurate, notably on lxbroy10 and vmnipkow9;
The file was modified src/Pure/Concurrent/multithreading.scala (diff)
Changeset 79604:0e8ac7db1f4d by wenzelm:
clarified num_processors: follow Poly/ML (with its inaccuracies);
The file was modified src/Pure/Concurrent/multithreading.ML (diff)
The file was modified src/Pure/Concurrent/multithreading.scala (diff)
Changeset 79603:9f002cdb6b8d by wenzelm:
clarified modules, following Isabelle/ML;
The file was addedsrc/Pure/Concurrent/multithreading.scala
The file was modified etc/build.props (diff)
The file was modified src/HOL/Tools/Nitpick/kodkod.scala (diff)
The file was modified src/Pure/Concurrent/isabelle_thread.scala (diff)
Changeset 79602:9ba800f12785 by wenzelm:
clarified signature;
The file was modified src/Pure/System/benchmark.scala (diff)
The file was modified src/Pure/System/host.scala (diff)
Changeset 79601:3430787e0620 by wenzelm:
tuned comments;
The file was modified src/Pure/Concurrent/multithreading.ML (diff)
Changeset 79600:d9eb4807557c by paulson:
merged
Changeset 79599:2c18ac57e92e by paulson _lp15@cam.ac.uk_:
the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses
The file was modified NEWS (diff)
The file was modified src/HOL/Analysis/Bochner_Integration.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Interval_Integral.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Integral_Substitution.thy (diff)
The file was modified src/HOL/Analysis/Set_Integral.thy (diff)
The file was modified src/HOL/Probability/Characteristic_Functions.thy (diff)
The file was modified src/HOL/Probability/Conditional_Expectation.thy (diff)
The file was modified src/HOL/Probability/Levy.thy (diff)
The file was modified src/HOL/Probability/Sinc_Integral.thy (diff)
Changeset 79598:66cbd1ef0db1 by paulson:
merged
Changeset 79597:76a1c0ea6777 by paulson _lp15@cam.ac.uk_:
A few lemmas brought in from AFP entries
The file was addedsrc/HOL/Library/Infinite_Typeclass.thy
The file was modified src/HOL/Fun.thy (diff)
The file was modified src/HOL/Fun_Def.thy (diff)
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/List.thy (diff)
Changeset 79596:1b3770369ee7 by traytel:
merged
Changeset 79595:3e27ab965a36 by traytel:
made destructor-view tactic more robust (by Jan van Brügge)
The file was modified src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML (diff)