[forgot to answer in particular] > inquit Brian: >> As long as we put off reintroducing 'a set as a separate type, we will >> continue to accumulate more theories (like Multivariate_Analysis) that >> confuse sets and predicates. The job of introducing 'a set will only >> get more difficult the longer we wait. I would certainly like to see >> the job completed before the next release, although it might require >> more time than we have.
I feel sympathetic with that concern, but I do not view that so
critical: according to what is currently going on in the repository, now
many contributors are aware to avoid set/pred mixture, and even so have
a personal interest to have the set type constructor back. For the
black matter outside there, the introduction of the set type constructor
is invasive anyway.
Cheers,
Florian
--
Home:
http://www.in.tum.de/~haftmann
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
