Am 13/02/2012 13:22, schrieb 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.
The irony is: if you had just added fold to List, without modifying foldl/r, it would have been less work for you and we could have discussed the unfication of the folds afterwards. Tobias _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
