[isabelle-dev] The Great Picard Theorem
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?
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev