[isabelle-dev] HOL iff notation

Makarius makarius at sketis.net
Tue Sep 3 16:21:55 CEST 2013

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 


More information about the isabelle-dev mailing list