[isabelle-dev] HOL iff notation

[Makarius]

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
>> Local_Theory.define).
>
> 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.)


 	Makarius