Re: [isabelle-dev] The Great Picard Theorem

2017-02-28 Thread Manuel Eberl
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

[isabelle-dev] NEWS (constant ii)

2017-02-28 Thread Lawrence Paulson
* Renamed ii to imaginary_unit in order to free up ii as a variable name. The syntax \ remains available. INCOMPATIBILITY. To my surprise, there are thousands of occurrences of ii throughout the library than the AFP. The overwhelming majority of these have nothing to do with the complex