[isabelle-dev] Finite_Set.filter clone of Set.project
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
> 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.
> you prefer the name »filter« over »project«, feel free to rename
> Set.project accordingly.
Done in 73ab6d4a9236.
More information about the isabelle-dev