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