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

Ondřej Kunčar kuncar at in.tum.de
Tue Oct 9 17:02:08 CEST 2012

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.


More information about the isabelle-dev mailing list