[isabelle-dev] typedef (open) unit

[Brian Huffman]

On Thu, Nov 18, 2010 at 2:59 PM, Makarius <makarius at sketis.net> wrote:
> 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.

If you think it is useful to have Isabelle/HOL provide a constant
Product_Type.unit == {True}, then by all means put it back in.

- Brian