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