[isabelle-dev] typedef (open) unit

Lawrence Paulson lp15 at cam.ac.uk
Fri Nov 19 11:51:50 CET 2010

It looks like something that I put in long ago, but honestly I cannot see a use for it.

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.

More information about the isabelle-dev mailing list