[isabelle-dev] Infinite_Set.thy

Lawrence Paulson lp15 at cam.ac.uk
Mon Nov 30 15:40:47 CET 2015

I have just checked, and this function is used nowhere in our libraries, including the AFP.

> On 27 Nov 2015, at 15:59, Tobias Nipkow <nipkow at in.tum.de> wrote:
> I remember other people suggesting this as well, albeit not on this list. It seems fair to me. Only the function atmost_one at the very end should go somewhere else.

More information about the isabelle-dev mailing list