[isabelle] typedef proof method


if i define a new type like 

typedef lessThree = ....

and i want to use this type definition as a proof method,

then "lessThree_def" doesnt work. I remember it was changed a bit, but i dont remember it exactly how it was. Can u help me?

Thank you!

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.