[isabelle-dev] HOL iff notation

Tobias Nipkow nipkow at in.tum.de
Mon Sep 2 16:29:34 CEST 2013

For uniformity I almost always use "=" and would not like to see it printed as <-->.


Am 02/09/2013 16:24, schrieb Makarius:
> (This is just a side-track on HOL notation, which came to me when cleaning up
> theories with old ASCII replacement syntax like & | --> <-> Un Int etc. -- which
> is very easy with explicit C+b completion in Isabelle/jEdit.)
> Isabelle/4379d46c8e13 (Oct 2005) introduces "alternative iff syntax for equality
> on booleans, with print_mode 'iff'".
> I can't remember a particular reason for the print mode, instead of having that
> syntax always on. I find myself using the "iff" notation most of the time to
> make theories look "nice".
> 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.)
>     Makarius
> _______________________________________________
> 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