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 gmail.com> wrote:
> 
> Hello!
> 
> I've introduced additional quantifier and rearranged some simple theorems
> in IFOL in similar fashion.
> 
> https://github.com/georgydunaev/onlyonequantifier/blob/master/my_IFOL.thy
> 
> 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.