[isabelle-dev] typedef (open) unit

Brian Huffman brianh at cs.pdx.edu
Fri Nov 19 00:05:22 CET 2010

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

More information about the isabelle-dev mailing list