[isabelle-dev] typedef (open) unit

[Makarius]

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.


 	Makarius