Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more hints;
  2. merged
  3. Added tag Isabelle2021 for changeset 7e2a9a8c2b85
  4. provide naproche-755224402e36;
  5. provide naproche-4ad61140062f;
  6. HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
  7. tidied up a few ugly proofs
  8. merged
  9. provide naproche-6d0d76ce2f2a;
  10. Added tag Isabelle2021-RC6 for changeset ed36e33a2e4b
  11. updated to flatlaf-1.0;
  12. tuned NEWS;
  13. tuned comments;
  14. more robust interrupt handling as in Future.forked_results (amending 64df1e514005);
  15. more parallelism: avoid exhaustion of standard thread pool;
Changeset 73258:fdc76c10bb61 by wenzelm:
more hints;
The file was modified Admin/Release/CHECKLIST
Changeset 73257:446085672b74 by wenzelm:
merged
Changeset 73256:69177d552afb by wenzelm:
Added tag Isabelle2021 for changeset 7e2a9a8c2b85
The file was modified .hgtags
Changeset 73255:7e2a9a8c2b85 by wenzelm:
provide naproche-755224402e36;
The file was modified Admin/components/components.sha1
Changeset 73254:13e206e93876 by wenzelm:
provide naproche-4ad61140062f;
The file was modified Admin/components/components.sha1
Changeset 73253:f6bb31879698 by manuel eberl _eberlm@in.tum.de_:
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
The file was addedsrc/HOL/Probability/Hoeffding.thy
The file was addedsrc/HOL/Probability/Product_PMF.thy
The file was modified CONTRIBUTORS
The file was modified NEWS
The file was modified src/HOL/Analysis/Bochner_Integration.thy
The file was modified src/HOL/Analysis/Borel_Space.thy
The file was modified src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
The file was modified src/HOL/Analysis/Set_Integral.thy
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy
The file was modified src/HOL/Probability/Central_Limit_Theorem.thy
The file was modified src/HOL/Probability/Conditional_Expectation.thy
The file was modified src/HOL/Probability/Giry_Monad.thy
The file was modified src/HOL/Probability/Independent_Family.thy
The file was modified src/HOL/Probability/Infinite_Product_Measure.thy
The file was modified src/HOL/Probability/Probability.thy
The file was modified src/HOL/Probability/Probability_Mass_Function.thy
The file was modified src/HOL/Probability/Probability_Measure.thy
Changeset 73252:b4552595b04e by paulson _lp15@cam.ac.uk_:
tidied up a few ugly proofs
The file was modified src/HOL/Complete_Partial_Order.thy
Changeset 73251:15ea7f6fb422 by wenzelm:
merged
Changeset 73250:e3e117660199 by wenzelm:
provide naproche-6d0d76ce2f2a;
The file was modified Admin/components/components.sha1
Changeset 73249:24494191e058 by wenzelm:
Added tag Isabelle2021-RC6 for changeset ed36e33a2e4b
The file was modified .hgtags
Changeset 73248:ed36e33a2e4b by wenzelm:
updated to flatlaf-1.0;
The file was modified Admin/components/components.sha1
The file was modified Admin/components/main
Changeset 73247:d92409f8203a by wenzelm:
tuned NEWS;
The file was modified NEWS
Changeset 73246:b9c480878663 by wenzelm:
tuned comments;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 73245:f69cbb59813e by wenzelm:
more robust interrupt handling as in Future.forked_results (amending 64df1e514005);
The file was modified src/Pure/System/scala.ML
Changeset 73244:5bded25065f8 by wenzelm:
more parallelism: avoid exhaustion of standard thread pool;
The file was modified src/Pure/System/bash.ML

Summary

  1. follow_on changes from Complex_Geometry
  2. merged
  3. a massive simplification, thanks to sledgehammer, etc.
  4. adapted to isabelle-dev/73253:f6bb31879698
  5. Buffons_Needle: tuned presentation
  6. Ergodic_Theory: removed 'pullback_algebra'. Turns out it already exists and is called 'vimage_algebra'.
Changeset 11633:4b87cdc4baaf by paulson _lp15@cam.ac.uk_:
follow_on changes from Complex_Geometry
The file was modified thys/Poincare_Disc/Poincare_Between.thy
The file was modified thys/Poincare_Disc/Poincare_Distance.thy
The file was modified thys/Poincare_Disc/Poincare_Lines.thy
The file was modified thys/Poincare_Disc/Poincare_Lines_Axis_Intersections.thy
The file was modified thys/Poincare_Disc/Poincare_Lines_Ideal_Points.thy
The file was modified thys/Poincare_Disc/Poincare_Tarski.thy
Changeset 11632:de4ae134bdf9 by paulson:
merged
Changeset 11631:ad3482c6e1ad by paulson _lp15@cam.ac.uk_:
a massive simplification, thanks to sledgehammer, etc.
The file was modified thys/Complex_Geometry/Chordal_Metric.thy
The file was modified thys/Complex_Geometry/Circlines.thy
The file was modified thys/Complex_Geometry/Hermitean_Matrices.thy
The file was modified thys/Complex_Geometry/Matrices.thy
The file was modified thys/Complex_Geometry/Moebius.thy
The file was modified thys/Complex_Geometry/More_Complex.thy
The file was modified thys/Complex_Geometry/More_Transcendental.thy
The file was modified thys/Complex_Geometry/Riemann_Sphere.thy
The file was modified thys/Complex_Geometry/Unitary11_Matrices.thy
The file was modified thys/Complex_Geometry/Unitary_Matrices.thy
Changeset 11630:547cd5ffe43f by manuel eberl _eberlm@in.tum.de_:
adapted to isabelle-dev/73253:f6bb31879698
The file was modified thys/Girth_Chromatic/Girth_Chromatic.thy
The file was modified thys/Random_Graph_Subgraph_Threshold/Prob_Lemmas.thy
The file was modified thys/Skip_Lists/Geometric_PMF.thy
The file was modified thys/Skip_Lists/Skip_List.thy
Changeset 11629:3ce2153720f3 by manuel eberl _eberlm@in.tum.de_:
Buffons_Needle: tuned presentation
The file was modified thys/Buffons_Needle/Buffons_Needle.thy
Changeset 11628:bcfe34497000 by manuel eberl _eberlm@in.tum.de_:
Ergodic_Theory: removed 'pullback_algebra'. Turns out it already exists and is called 'vimage_algebra'.
The file was modified thys/Ergodic_Theory/ME_Library_Complement.thy
The file was modified thys/Ergodic_Theory/Shift_Operator.thy