Changes

Summary

Moved up a theorem
Limit properties for complex exponential
More of Eberl's contributions: memomorphic functions
merged
New material due to Eberl on Formal Laurent Series
merged
A bit more tidying and some new material

Changeset 77279:c16d423c9cb1 by paulson _lp15@cam.ac.uk_: Moved up a theorem
The file was modified	`src/HOL/Analysis/Complex_Transcendental.thy` (diff)
The file was modified	`src/HOL/Library/Periodic_Fun.thy` (diff)
Changeset 77278:e20f5b9ad776 by paulson _lp15@cam.ac.uk_: Limit properties for complex exponential
The file was modified	`src/HOL/Complex.thy` (diff)
Changeset 77277:c6b50597abbc by paulson _lp15@cam.ac.uk_: More of Eberl's contributions: memomorphic functions
The file was added	`src/HOL/Complex_Analysis/Laurent_Convergence.thy`
The file was added	`src/HOL/Complex_Analysis/Meromorphic.thy`
The file was modified	`src/HOL/Complex_Analysis/Complex_Analysis.thy` (diff)
The file was modified	`src/HOL/Complex_Analysis/Complex_Singularities.thy` (diff)
The file was modified	`src/HOL/Complex_Analysis/Residue_Theorem.thy` (diff)
The file was modified	`src/HOL/Complex_Analysis/Riemann_Mapping.thy` (diff)
The file was modified	`src/HOL/Complex_Analysis/Winding_Numbers.thy` (diff)
The file was modified	`src/HOL/Library/Landau_Symbols.thy` (diff)
Changeset 77276:29032b496f2e by paulson: merged
Changeset 77275:386b1b33785c by paulson _lp15@cam.ac.uk_: New material due to Eberl on Formal Laurent Series
The file was modified	`src/HOL/Analysis/Complex_Transcendental.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Formal_Laurent_Series.thy` (diff)
The file was modified	`src/HOL/Filter.thy` (diff)
Changeset 77274:05ad117ee3fb by paulson: merged
Changeset 77273:f82317de6f28 by paulson _lp15@cam.ac.uk_: A bit more tidying and some new material
The file was modified	`src/HOL/Analysis/Complex_Transcendental.thy` (diff)
The file was modified	`src/HOL/Analysis/Elementary_Metric_Spaces.thy` (diff)