[isabelle-dev] HOL iff notation

[Lawrence Paulson]

To me, the ability to use = (on booleans) as an alternative to <-> is an artefact of HOL, rather than something to encourage. Almost always, <-> is more readable. At least that's my view.

Larry

On 2 Sep 2013, at 19:42, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:

>> Are there clubs of "iff" vs. "non-iff"?  If almost everybody is a member
>> of the "iff" club we could just remove that print mode.  (We don't have
>> to consider that for the coming release, to avoid any real-time pressure
>> on this question.)
> 
> I am definitely a member of the iff-club.  Partly for precedence
> reasons, but also because you can recognize predicate equations immediately.