>> I wonder whether it is wise to have three of these. People are going to >> attach more significance to them than they deserve. I am inclined to >> think that we should get rid of arbitrary. >> Larry
I also think that two would be better than three; technically "undefined" is the same as "arbitrary", and IMHO only one one variant should persist. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de -------------- next part -------------- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 252 bytes Desc: OpenPGP digital signature URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20081003/99ecb587/attachment.pgp>