> On 27 Dec 2018, at 12:45, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote: > > (I don't know how useful the strict versions less_poll, greater_poll > would be). Strict versions do turn up in some places (both in HOL Light and Isabelle/ZF)