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

[Ondřej Kunčar]

On 10/06/2012 04:04 PM, Florian Haftmann wrote:
> 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.

Thanks for pointing to this.

> Would there be any obstacle to use Set.project consistently instead?

Done in 718f10c8bbfc.

> If
> you prefer the name »filter« over »project«,  feel free to rename
> Set.project accordingly.

Done in 73ab6d4a9236.

Ondrej