I have just added this to the Analysis directory, making its inevitable
refactoring more necessary.
Arguably it should be an AFP entry. Unfortunately, I’m not sufficiently expert
in complex analysis to say whether it is core material or not. It looks like a
fundamental result to me.
We should probably resolve the question of Analysis before the next release.
How do we decide which things go into Complex_Main versus Analysis (which could
be split into basic/advanced) and the AFP?
isabelle-dev mailing list