Re: [isabelle] Tiny minor backward-compatible changes to IFOL

Thank you for your email. I think you are right that a uniqueness quantifier is useful to have, for Isabelle/HOL as well as for FOL. We are likely to introduce such a thing. While we welcome contributions, they should normally take the form of small snippets of new material as opposed to entire revised files.

Larry Paulson

> On 26 Apr 2020, at 11:00, Georgy Dunaev <georgedunaev at> wrote:
> Hello!
> I've introduced additional quantifier and rearranged some simple theorems
> in IFOL in similar fashion.
> I just thought that it would be elegant to have E!x.P(x) as a Ex.P(x) and
> !x.P(x), wouldn't be it? :) Moreover, this kind of definition is considered
> to be "safe" later.(Why?) You may ask me to make additional changes if you
> find that something is worth doing.
> Kind regards,
> Georgy Dunaev

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