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 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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev