[isabelle-dev] HOL iff notation
Gerwin.Klein at nicta.com.au
Tue Sep 3 01:39:30 CEST 2013
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.
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.
More information about the isabelle-dev