[isabelle-dev] Finite_Set.filter clone of Set.project

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sat Oct 6 16:04:41 CEST 2012

Hi Ondrej,

I stumbled over


where you have introduced Finite_Set.fold which on finite sets is equal
to Set.project (cf.
http://isabelle.in.tum.de/repos/isabelle/rev/558e4e77ce69#l1.41) and on
infinite sets is underspecified.

Would there be any obstacle to use Set.project consistently instead?  If
you prefer the name »filter« over »project«, feel free to rename
Set.project accordingly – the tradition there is not so deep-rooted yet.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 259 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20121006/31b84b14/attachment.asc>

More information about the isabelle-dev mailing list