[isabelle-dev] HOL iff notation

[Lawrence Paulson]

I tend to use <->, but I'm afraid I don't know what a print mode is.
Larry

On 2 Sep 2013, at 15:29, Tobias Nipkow <nipkow at in.tum.de> wrote:

> For uniformity I almost always use "=" and would not like to see it printed as <-->.
> 
> Tobias
> 
> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev