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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
