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).
Regular 'definition' is just another derived mechanism like 'theorem',
'inductive', 'function' etc. You first claim some propositions, the
system somehow provides foundations in the background, and you get
theorems back. The construction + proof happens to be relatively simple
for 'definition', but it is there nonetheless.
The old 'defs' command still provides access to primitive definitions at
the bare metal -- for historical and nostalgic reasons. We might start
thinking if it is time to discontinue it, or what is missing towards that
step. (We've got rid of old 'axioms' already, and hardly anyone has
noticed.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
