[isabelle-dev] HOL iff notation

[Lars Noschinski]

On 03.09.2013 16:21, Makarius wrote:
> On Tue, 3 Sep 2013, Lawrence Paulson wrote:
>
>> For sure. I think it confuses beginners at first, because == is only
>> allowed in "real" definitions rather than derived ones.
>
> "Real" definitions are actually just for foundational purposes: users
> never see them -- neither end-users nor users in the sense of other
> tools built on top of the system infrastructure (notably
> Local_Theory.define).

As long as "def" and "defines" require "==", I don't see much reason in 
abandoning "==" for "definition" in my own usage.

(Actually, I would even prefer to use == even for fun and primrec, as it 
has a better priority for these purposes.)

   -- Lars