[isabelle-dev] HOL iff notation

[Makarius]

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