[isabelle-dev] The HOL Light library

Lawrence Paulson lp15 at cam.ac.uk
Thu Oct 6 15:18:50 CEST 2016

And now that I have managed to prove “invariance of domain”, a significant if not especially famous result.

> On 6 Oct 2016, at 14:08, Makarius <makarius at sketis.net> wrote:
> Definitely. It is probably worth a line to the ANNOUNCE file for
> Isabelle2016-1.

More information about the isabelle-dev mailing list