On Thu, Nov 18, 2010 at 2:59 PM, Makarius <[email protected]> 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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
