Re: [isabelle] Any users of "Old_Datatype.thy" or "Old_SMT.thy"?
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.
From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Jasmin Blanchette <jasmin.blanchette at inria.fr>
Sent: 28 December 2016 16:16:46
To: Isabelle Users
Subject: [isabelle] Any users of "Old_Datatype.thy" or "Old_SMT.thy"?
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