[isabelle-dev] typedef (open) unit

[Makarius]

On Thu, 18 Nov 2010, Brian Huffman wrote:

> 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.

I don't know if that is useful.

The point here is that formally it is a non-conservative change deep down 
in the guts of HOL.  Such things routinely cause surprises much later. 
This means there must be a good reasong for the change -- a documented one 
so others have a chance to review it quickly, without a long and tedious 
thread on the mailing list.


 	Makarius