duplicate words removed from various documentation files

The magic command is:

grep " \([[:alpha:]]\+\) \1[[:space:]]" \
`find . -name "*.doc" -or -name "*.tex"`

but the output still needs to be filtered by eye, since many duplicates
occur in embedded math and ML.

Duplicates in the Italian manual approved by Domenico Masini.

consistent use of upper-case letters within enumeration

Tuned.

Start working on porting the doc building system to SML (i.e., not Moscow ML)
to get it working with Poly ML.