Re: [isabelle] Any users of "Old_Datatype.thy" or "Old_SMT.thy"?

Dear Jasmin,

I am not sure what the latest states of Nominal1 (in the distribution) and Nominal2 (in the AFP) are? If I remember correctly, they depend internally

on old_datatype (heavily). I am not sure how easy it would be to port

them to (new)datatype. It would certainly be desirable.

Best wishes,


From: cl-isabelle-users-bounces at <cl-isabelle-users-bounces at> on behalf of Jasmin Blanchette <jasmin.blanchette at>
Sent: 28 December 2016 16:16:46
To: Isabelle Users
Subject: [isabelle] Any users of "Old_Datatype.thy" or "Old_SMT.thy"?

Hi all,

The "datatype" command and the "smt" proof method were reimplemented in Isabelle2014. For compatibility, the old constructs are provided by "~~/src/HOL/Library/Old_Datatype.thy" and "~~/src/HOL/Library/Old_SMT.thy", as "old_datatype" and "old_smt".

1. Do you depend on either of these constructs?

2. If so, why?

3. Would you be sorry if "old_datatype", "old_smt", or both were to be missing in the next release (presumably Isabelle2017)?

If the answer to question 3 is yes, please reply.


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