Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] typedef proof method

view this post on Zulip Email Gateway (Aug 19 2022 at 13:29):

From: "Roger H." <s57076@hotmail.com>
Hi,

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!

Last updated: Nov 21 2024 at 12:39 UTC