[isabelle-dev] HOL iff notation

[Peter Lammich]

Almost always I use <-->. The only exception being a comparison of
booleans, like in "if (a::bool) = b then ..."

-- Peter


On Di, 2013-09-03 at 09:33 +0900, Christian Sternagel wrote:
> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev