# HG changeset patch # User paulson # Date 1710260392 0 # Node ID 0e9a809dc0b2353621ac845dc6d0b5f608a514a5 # Parent 53d0d2860ed855cdfb308df73794e7339234435b Restored Riemann_Mapping as an import of Complex_Analysis diff -r 53d0d2860ed8 -r 0e9a809dc0b2 src/HOL/Complex_Analysis/Complex_Analysis.thy --- a/src/HOL/Complex_Analysis/Complex_Analysis.thy Tue Mar 12 12:11:39 2024 +0000 +++ b/src/HOL/Complex_Analysis/Complex_Analysis.thy Tue Mar 12 16:19:52 2024 +0000 @@ -1,5 +1,6 @@ theory Complex_Analysis -imports + imports + Riemann_Mapping Residue_Theorem Meromorphic begin