Re: [isabelle] NBG in Isabelle/HOL?

> On 17 May 2020, at 12:27, Lawrence Paulson <lp15 at> wrote:
> It’s main drawback is that you simply write a formula when specifying a subset (via the separation axiom), forcing you to find an encoding using a combinator language. 

Sorry, important correction: “you CANNOT simply write a formula” (such as f(x)=g(x) & x>0).

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.