[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