[isabelle-dev] "canonical" left-fold combinator for lists

[Florian Haftmann]

>> Anyway, personally I have no strong opinion about this, so anybody who
>> wants to get hands on should feel invited to do so.
>
> It would have been better to discuss such a change beforehand rather
> than make it and then say that we are welcome to modify it.

Please recall:

> The movement of the code setup for sets into the HOL-Main corpus also
> brought this fold into List.thy.

The task of introducing 'a set as type constructor was, as I still deem, 
too ambitious to depend on such a detail as the introduction of an 
additional definition into List.thy.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de