[isabelle-dev] HOL iff notation
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