Thanks for replies.
@Nick - I too am measuring around 0.7V on pin 13.
@Woody - That is exactly what I did, and it does work. I just assumed that the LED would be turned off unless explicitly set to HIGH.
@Nick - putting
in the loop without
in the setup does not change anything - the LED stays lit.
However, putting just
in the setup, and nothing else in the loop works - LED is turned off.
So, it seems that it is normal for pin 13 LED to be dimly lit. I just did not perceive it as dim - it is almost as bright as ON, TX or RX LEDs. I do not see any difference when lighting it with 5V (pin 13 set as OUTPUT and set to HIGH) or 0.7V (pin 13 in its default INPUT state).