Miscellaneous minor changes. mostly for clarity: