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