Change USBTX/RX to CONSOLE_TX/RX

Author: gpsimenos

docs/porting/standard_pin_names/pin_names_dev_guide.md

@@ -61,4 +61,4 @@ However, these names do not apply to all boards and hence should not be used in
 
 Every Mbed board includes a serial interface to the host PC, which allows the console to print useful information about the application.
 
-The pins for the main serial interface are defined as `USBTX` and `USBRX`.
+The pins for the main serial interface are defined as `CONSOLE_TX` and `CONSOLE_RX`.

docs/porting/standard_pin_names/pin_names_porting.md

@@ -9,7 +9,7 @@ There is a set of generic guidelines that apply to all boards, and further sets
 The generic guidelines currently define rules for the naming of LED pins, button pins and UART pins. In summary, the rules are:
 * LED pins are defined as `LEDx` (e.g. `LED0`, `LED1`)
 * Button pins are defined as `BUTTONx` (e.g. `BUTTON0`, `BUTTON1`)
-* UART pins for console communication with host are defined as `USBTX` and `USBRX`
+* UART pins for console communication with host are defined as `CONSOLE_TX` and `CONSOLE_RX`
 * Pin aliases are allowed (e.g. `#define RED_LED LED1`)
 * Pin definitions must be a `#define`, not an `enum`
 * A physical MCU pin can be assigned to no more than one LED, button or UART pin definition