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

Reply via email to