Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. More analysis / measure theory material
  2. merged
  3. more new material about analysis
  4. added forgotten declaration provided by Florian Haftmann
Changeset 70380:2b0dca68c3ee by paulson _lp15@cam.ac.uk_:
More analysis / measure theory material
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Normed_Spaces.thy (diff)
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/Measure_Space.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
Changeset 70379:8a7053892d8e by paulson:
merged
Changeset 70378:ebd108578ab1 by paulson _lp15@cam.ac.uk_:
more new material about analysis
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Ordered_Euclidean_Space.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Library/Liminf_Limsup.thy (diff)
The file was modified src/HOL/NthRoot.thy (diff)
Changeset 70377:04f492d004fa by nipkow:
added forgotten declaration provided by Florian Haftmann
The file was modified src/HOL/Library/Code_Real_Approx_By_Float.thy (diff)