[isabelle-dev] typedef (open) unit

Makarius makarius at sketis.net
Fri Nov 19 11:43:11 CET 2010

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.


More information about the isabelle-dev mailing list