[isabelle-dev] HOL iff notation
lp15 at cam.ac.uk
Mon Sep 2 16:34:31 CEST 2013
I tend to use <->, but I'm afraid I don't know what a print mode is.
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 <-->.
> 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.)
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev