[isabelle-dev] HOL iff notation

Lawrence Paulson lp15 at cam.ac.uk
Tue Sep 3 11:31:46 CEST 2013

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

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.

More information about the isabelle-dev mailing list