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

Makarius makarius at sketis.net
Tue Jul 28 17:40:34 CEST 2015


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


More information about the isabelle-dev mailing list