Recently I have been trying to find the definition of the subsystem $ATR_0$ of second-order arithmetic. Only "definitions" I have found were quite vague, like informal definition on Wikipedia which says it's $ACA_0$ plus statement that "any arithmetical functional can be iterated transfinitely along any countable well ordering starting with any set", or some paper claiming that $ATR_0$ is just $ACA_0$+"for every ordinal $\alpha<\omega_1^\text{CK}$ $\emptyset^{(\alpha)}$ exists". Can anyone point me to the *formal* definition of this system?

Thanks in advance.