[isabelle-dev] cardinality primitives in Isabelle/HOL?

Lawrence Paulson lp15 at cam.ac.uk
Thu Dec 27 14:57:56 CET 2018

> 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)

More information about the isabelle-dev mailing list