Issue 4925: Don't use @code inside of @example

Issue 4925: Don't use @code inside of @example

@example is already set in monospace font (use @display if you don't
want to change fonts).  This replacement was done mechanically using
the script

    sed -i '/@example *$/,/@end example *$/{s/@code{\(\([^@}]\|@[@{}]\)*\)}/\1/g;s/ \+$//;}' $(git grep -l '^@end example$' Documentation)

so not all replacements are really formatted best.  But overall this
looks like an improvement.