Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. meta_digest without accidental source positions (amending 1544e61e5314): avoid spurious rebuild of unrelated sessions after editing ROOT;
  2. Fixed LaTeX issue
  3. New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
  4. instance for polynomial rings with characteristic zero
Changeset 65580:66351f79c295 by wenzelm:
meta_digest without accidental source positions (amending 1544e61e5314): avoid spurious rebuild of unrelated sessions after editing ROOT;
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 65579:52eafedaf196 by paulson _lp15@cam.ac.uk_:
Fixed LaTeX issue
The file was modified src/HOL/Complex.thy (diff)
Changeset 65578:e4997c181cce by paulson _lp15@cam.ac.uk_:
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Complex_Transcendental.thy (diff)
The file was modified src/HOL/Analysis/Conformal_Mappings.thy (diff)
The file was modified src/HOL/Analysis/Gamma_Function.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Poly_Roots.thy (diff)
The file was modified src/HOL/Analysis/Summation_Tests.thy (diff)
The file was modified src/HOL/Analysis/Weierstrass_Theorems.thy (diff)
The file was modified src/HOL/Complex.thy (diff)
The file was modified src/HOL/Computational_Algebra/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Decision_Procs/Approximation.thy (diff)
The file was modified src/HOL/Filter.thy (diff)
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/Probability/Sinc_Integral.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
Changeset 65577:32d4117ad6e8 by haftmann:
instance for polynomial rings with characteristic zero
The file was modified src/HOL/Computational_Algebra/Polynomial.thy (diff)