[isabelle-dev] The Great Picard Theorem

[Lawrence Paulson]

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?

Larry