[isabelle-dev] The Great Picard Theorem

Lawrence Paulson lp15 at cam.ac.uk
Wed Feb 22 17:46:36 CET 2017

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?


More information about the isabelle-dev mailing list