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.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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. 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
Isabelle2016-1.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[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 the next 
release.

Larry

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev