[isabelle-dev] HOL iff notation

Christian Sternagel c.sternagel at gmail.com
Tue Sep 3 02:33:20 CEST 2013

Same here. - cheers chris

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.
>	Florian
>PGP available:
>isabelle-dev mailing list
>isabelle-dev at in.tum.de

More information about the isabelle-dev mailing list