Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more de-applying
  2. patched a continuity proof
  3. merged
  4. de-applying, etc.
  5. moved lemmas
Changeset 68614:3cb44b0abc5c by paulson _lp15@cam.ac.uk_:
more de-applying
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HSEQ.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
Changeset 68613:2fae3e01a2ec by paulson _lp15@cam.ac.uk_:
patched a continuity proof
The file was modified src/HOL/Probability/Sinc_Integral.thy (diff)
Changeset 68612:ffc3fd6c7498 by paulson:
merged
Changeset 68611:4bc4b5c0ccfc by paulson _lp15@cam.ac.uk_:
de-applying, etc.
The file was modified src/HOL/Analysis/Inner_Product.thy (diff)
The file was modified src/HOL/Analysis/Product_Vector.thy (diff)
The file was modified src/HOL/Deriv.thy (diff)
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HLim.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HTranscendental.thy (diff)
The file was modified src/HOL/NthRoot.thy (diff)
The file was modified src/HOL/Power.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
Changeset 68610:4fdc9f681479 by nipkow:
moved lemmas
The file was modified src/HOL/Analysis/Extended_Real_Limits.thy (diff)
The file was modified src/HOL/Conditionally_Complete_Lattices.thy (diff)
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Nat.thy (diff)