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

[Florian Haftmann]

Hi Ondrej,

I stumbled over

http://isabelle.in.tum.de/repos/isabelle/rev/558e4e77ce69

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.

Best,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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