[isabelle-dev] HOL iff notation

[Lawrence Paulson]

For sure. I think it confuses beginners at first, because == is only allowed in "real" definitions rather than derived ones.
Larry

On 3 Sep 2013, at 00:39, Gerwin Klein <Gerwin.Klein at nicta.com.au> wrote:

> 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.