[isabelle-dev] The Great Picard Theorem

Manuel Eberl eberlm at in.tum.de
Tue Feb 28 11:58:21 CET 2017

I'm not an expert in complex analysis either, but do remember that it
was briefly mentioned ā€“ but not proved ā€“ in my introductory lecture on
Complex Analysis when I was an undergratuate.

My intuition tells me that this is a very beautiful result, but not one
that you need a lot, but I could be wrong about this.

I could perhaps ask around a bit.

I for one am quite open to the idea of moving more material from the
distribution to the AFP, especially from HOL-Analysis. Picard's theorem
sounds like a reasonable candidate for that, but in general, I also have
no idea where to draw the line.



On 22/02/17 17:46, Lawrence Paulson wrote:
> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list