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.
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
