Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. quite a few more results about negligibility, etc., and a bit of tidying up
  2. merged
  3. a few more results
  4. added bottom-up merge sort
  5. various new results on measures, integrals, etc., and some simplified proofs
Changeset 67986:b65c4a6a015e by paulson _lp15@cam.ac.uk_:
quite a few more results about negligibility, etc., and a bit of tidying up
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Determinants.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Inner_Product.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Analysis/Weierstrass_Theorems.thy (diff)
Changeset 67985:7811748de271 by paulson:
merged
Changeset 67984:adc1a992c470 by paulson _lp15@cam.ac.uk_:
a few more results
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
Changeset 67983:487685540a51 by nipkow:
added bottom-up merge sort
The file was modified src/HOL/Data_Structures/Sorting.thy (diff)
Changeset 67982:7643b005b29a by paulson _lp15@cam.ac.uk_:
various new results on measures, integrals, etc., and some simplified proofs
The file was modified src/HOL/Analysis/Ball_Volume.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Complete_Measure.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Fashoda_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Linear_Algebra.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Analysis/Sigma_Algebra.thy (diff)
The file was modified src/HOL/Probability/Information.thy (diff)