[isabelle-dev] The HOL Light library

Makarius makarius at sketis.net
Thu Oct 6 15:08:19 CEST 2016

On 03/10/16 15:16, Lawrence Paulson wrote:
> I’ve just added a lot more advanced material from HOL Light. There isn't much about this in the NEWS file; unfortunately there is no headline result to mention or even a dominant theme. Nor can we say that the entire library has been ported. But I still think it’s a significant development for the next release.

Definitely. It is probably worth a line to the ANNOUNCE file for


More information about the isabelle-dev mailing list