Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. clarified standardization of variables, with proper treatment of local variables; tuned signature; tuned;
  3. removal of more redundancies, and fixes
  4. merged
  5. elimination of near duplication involving Rolle's theorem and the MVT
Changeset 69024:287bb00371c1 by wenzelm:
merged
Changeset 69023:cef000855cf4 by wenzelm:
clarified standardization of variables, with proper treatment of local variables;<br>tuned signature;<br>tuned;
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/Thy/export_theory.scala (diff)
The file was modified src/Pure/drule.ML (diff)
The file was modified src/Pure/logic.ML (diff)
The file was modified src/Pure/term_subst.ML (diff)
Changeset 69022:e2858770997a by paulson _lp15@cam.ac.uk_:
removal of more redundancies, and fixes
The file was modified src/HOL/Analysis/Borel_Space.thy (diff)
The file was modified src/HOL/Computational_Algebra/Polynomial.thy (diff)
The file was modified src/HOL/Deriv.thy (diff)
The file was modified src/HOL/MacLaurin.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
Changeset 69021:4dee7d326703 by paulson:
merged
Changeset 69020:4f94e262976d by paulson _lp15@cam.ac.uk_:
elimination of near duplication involving Rolle&#039;s theorem and the MVT
The file was modified src/HOL/Analysis/Derivative.thy (diff)
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/Deriv.thy (diff)
The file was modified src/HOL/MacLaurin.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)