Stream: Beginner Questions

Topic: Old style datatypes

view this post on Zulip Julin Shaji (Feb 17 2025 at 09:27):

When trying to figure out what datatype_compat meant, I came across a mention of 'old-style datatypes' and associated plugins at
https://isabelle.in.tum.de/library/Doc/Datatypes/Datatypes.html

What is the difference between old style and new style datatypes?
Is this difference something that isabelle users need to be aware of?

Is there some place where we can read more about it?

view this post on Zulip Jan van Brügge (Feb 17 2025 at 09:43):

datatype_compat is only for backwards compatibility. The new ones (ie the normal datatype) command do everything the old ones did and more. There is no reason to use or read into the old ones

view this post on Zulip Julin Shaji (Feb 17 2025 at 10:28):

Jan van Brügge said:

or read into the old ones

Is the theory at https://isabelle.in.tum.de/library/Doc/Datatypes/Datatypes.html old?

view this post on Zulip Jan van Brügge (Feb 17 2025 at 16:02):

No, those are the new ones.

Last updated: Mar 09 2025 at 12:28 UTC