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 <[email protected]> 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 >> [email protected] >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
