Changes

Summary

New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series

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)