[isabelle-dev] HOL iff notation
noschinl at in.tum.de
Tue Sep 3 16:44:48 CEST 2013
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
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.)
More information about the isabelle-dev