Re: [isabelle] NBG in Isabelle/HOL?



Dear Lawrence Paulson,

Thank you for providing the remark. I did struggle to understand the
intended meaning/significance of the first part of the sentence, but
the meaning of the message could still be inferred from the second part, in
conjunction with what I have seen based on the content of the repository
that I mentioned in my question.

Kind Regards,
Mikhail Chekhov

On Mon, May 18, 2020 at 12:08 PM Lawrence Paulson <lp15 at cam.ac.uk> wrote:

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