[isabelle-dev] HOL iff notation

[Gerwin Klein]

On 03/09/2013, at 12:24 AM, Makarius <makarius at sketis.net> 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 like both. I mostly use "=", because it is less typing. I usually prefer output being equal to input, but I will use <-> for presentation occasionally (in that sense, the print mode is ideal for me).

I also still use == quite a bit, I never understood why it is discouraged so much. It has the better precedence, and I use it mostly for the difference between a definition and an equation, which non-Isabelle people seem to understand.

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.