[isabelle-dev] HOL iff notation
lp15 at cam.ac.uk
Mon Sep 2 20:55:30 CEST 2013
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.
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.
More information about the isabelle-dev