[isabelle-dev] HOL iff notation
makarius at sketis.net
Tue Sep 3 16:57:06 CEST 2013
On Tue, 3 Sep 2013, Lars Noschinski wrote:
> 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.
That is just a historical left-over. Both 'def' and 'defines' are
relatively unimportant in practice, so the renovation plan for them to
conform to 'definition' (with its preprocessor) has a low priority -- it
is there nonetheless.
In fact, live of everybody in infrastructure building would be much easier
without 'defines'. (This is just speculative right now -- nothing for
this release. Just a reminder that old stuff is still there to be cleaned
up eventually, to get the important things right, and leave the
unimportant ones behind.)
More information about the isabelle-dev