How do I rename the extension for a bunch of files?

If using bash, there’s no need for external commands like sed, basename, rename, expr, etc.

for file in *.html
do
  mv "$file" "${file%.html}.txt"
done