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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
