On 06.10.2010 12:17, Palle Raabjerg wrote:
So yes, is there an actual finite set datatype, or would it be possible to define one? Or must I use lists in the nominal datatype to somehow emulate finite sets?
There is the theory Fset in library which defines a finite set type. -- Lars