I have just checked, and this function is used nowhere in our libraries, including the AFP. Larry > 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.