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
