And now that I have managed to prove “invariance of domain”, a significant if
not especially famous result.
Larry
> On 6 Oct 2016, at 14:08, Makarius wrote:
>
> Definitely. It is probably worth a line to the ANNOUNCE file for
> Isabelle2016-1.
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.
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