Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Merge
  2. new material connected with HOL Light measure theory, plus more rationalisation
Changeset 63953:b5d7806c9396 by paulson _lp15@cam.ac.uk_:
Merge
Changeset 63952:354808e9f44b by paulson _lp15@cam.ac.uk_:
new material connected with HOL Light measure theory, plus more rationalisation
The file was modified src/HOL/Analysis/Borel_Space.thy (diff)
The file was modified src/HOL/Analysis/Bounded_Linear_Function.thy (diff)
The file was modified src/HOL/Analysis/Derivative.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Gamma_Function.thy (diff)
The file was modified src/HOL/Deriv.thy (diff)
The file was modified src/HOL/Fields.thy (diff)
The file was modified src/HOL/Groups_Big.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/Order_Relation.thy (diff)
The file was modified src/HOL/Probability/Helly_Selection.thy (diff)
The file was modified src/HOL/Probability/Weak_Convergence.thy (diff)
The file was modified src/HOL/Series.thy (diff)
The file was modified src/HOL/Set.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)