Re: [isabelle] Tiny minor backward-compatible changes to IFOL
- To: Georgy Dunaev <georgedunaev at gmail.com>
- Subject: Re: [isabelle] Tiny minor backward-compatible changes to IFOL
- From: Lawrence Paulson <lp15 at cam.ac.uk>
- Date: Wed, 6 May 2020 17:03:16 +0100
- Cc: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
- In-reply-to: <CAAMrf_2Uq8zG6oOZZCV+jQeoncdp9WLqaTkZRMUjf4h79FraWg@mail.gmail.com>
- References: <CAAMrf_2Uq8zG6oOZZCV+jQeoncdp9WLqaTkZRMUjf4h79FraWg@mail.gmail.com>
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.
> On 26 Apr 2020, at 11:00, Georgy Dunaev <georgedunaev at gmail.com> wrote:
> 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