Re: [isabelle-dev] The HOL Light library

2016-10-06 Thread Lawrence Paulson
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.

Re: [isabelle-dev] The HOL Light library

2016-10-06 Thread Makarius
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.

[isabelle-dev] The HOL Light library

2016-10-03 Thread Lawrence Paulson
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