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

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Mon Feb 13 13:22:18 CET 2012

>> 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.



PGP available:

More information about the isabelle-dev mailing list