[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.