[isabelle-dev] NEWS: Cauchy's integral theorem

[Larry Paulson]

I couldn’t possibly give a percentage. On the one hand, I would guess that most of Multivariate_Analysis comes from the HOL Light libraries. Maybe some of Probability as well, although originally it came from HOL4.

What I have just added is about the first 20% of the file cauchy.ml. The remaining 80% includes a development of winding numbers and quite a few other theorems. Probably most of them come from the famous list of 100 theorems. Other results, including the prime number theorem, are other files. None of these proofs are pretty. Puzzling them out is brain-bending.

Larry

> On 28 Jul 2015, at 16:40, Makarius <makarius at sketis.net> wrote:
> 
> On Tue, 28 Jul 2015, Larry Paulson wrote:
> 
>> Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals and Cauchy's integral theorem,
>>   ported from HOL Light
>> 
>> There is much more that could be added here, assuming I don’t run out of energy!
> 
> What is your estimate of the percentage of all material by John Harrison in HOL-Light that has been ported to Isabelle/HOL already?
> 
> 
> 	Makarius