[isabelle-dev] "canonical" left-fold combinator for lists
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.
> 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.
More information about the isabelle-dev