It looks like something that I put in long ago, but honestly I cannot see a use for it.
Larry
On 19 Nov 2010, at 10:43, Makarius wrote:
>> 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.