Re: [isabelle] NBG in Isabelle/HOL?



> On 17 May 2020, at 12:27, Lawrence Paulson <lp15 at cam.ac.uk> 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.