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 <nip...@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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
