[isabelle-dev] typedef (open) unit

Makarius makarius at sketis.net
Thu Nov 18 23:59:30 CET 2010

On Thu, 18 Nov 2010, Brian Huffman wrote:

> The effect of my change "typedef (open) unit" is to remove the
> definition of the following constant
> unit_def: "unit == {True}"
> thus making the name "unit" available to users.

So this is a name space thing only?  Maybe hide_const would do the job.

Historically, we could not hide it because it was "global", but Florian 
has purged that recently.


More information about the isabelle-dev mailing list