[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:
>http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
>
>_______________________________________________
>isabelle-dev mailing list
>isabelle-dev at in.tum.de
>https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


More information about the isabelle-dev mailing list