Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. imported new material mostly due to Sébastien Gouëzel
Changeset 70723:4e39d87c9737 by paulson _lp15@cam.ac.uk_:
imported new material mostly due to Sébastien Gouëzel
The file was modified src/HOL/Analysis/Elementary_Metric_Spaces.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/Finite_Set.thy (diff)
The file was modified src/HOL/Groups_Big.thy (diff)
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/CLim.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HDeriv.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HLim.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HLog.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HyperDef.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/NSA.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/NSComplex.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
The file was modified src/HOL/Series.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)