Hi Jasmin, > There will be a high level of compatibility between the old and the new package. > For nonnested recursive datatypes, compatibility is quasi-100%; and for nested > datatypes, the package will support an optional "nested to mutual" reduction > to > simulate the old package, so that the same theorems as before are available > (albeit under different names).
has an explicit need for a »nested to mutual« mode ever been
articulated? In my personal opinion this construction has always
appeared counter-intuitive, because the inherent redundancy with an
existing type springs to your eyes after you have done this game a few
times. Maybe a chance to save some work.
> A rough, optimistic time plan follows.
Overall, a realistic and reasonable schedule.
> October--December 2013 (?):
> Release Isabelle2013-1 with both "datatype" and "datatype_new"
>
> Spring 2014:
> Rename {"datatype" |-> "legacy_datatype", "datatype_new" |-> "datatype"}
>
> Summer/Fall 2014:
> Release Isabelle2014 with both "legacy_datatype" and "datatype"
Is there any experimental evicdence how many datatype specifications
would break by a drop-in replacement (real applications, not
demonstration examples)? If this is significantly little, I would even
think about doing the switch {"datatype" |-> "legacy_datatype",
"datatype_new" |-> "datatype"} immediately. The »_new« suffix has a
strange connotation of »almost done… ad multos annos«.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
