Reading Chris Hankin's book, "An Introduction to Lambda Calculus for Computer Scientists", I learnt that the rules for reductions in the pure $\lambda$-Calculus are the $\beta$-reduction rule, $$(\lambda x.M)N = M[x:= N]$$ and also these: $$\frac{M=N}{N=M}$$ $$\frac{M=N}{MZ=NZ}$$ $$\frac{M=N}{ZM=ZN}$$ $$\frac{M=N}{\lambda x.M = \lambda x.N}$$ The author calls this "The Theory $\lambda$"; and although he formally defines contexts, he does not use them there.
Now, some other works -- for example, Didier Rémy's "Type Systems for Programming languages" -- seem to imply that there are only the $\beta$-reduction rule, and a context-rule: $$(\lambda x.a)v \to a[x:= v]$$ $$\frac{a\to a'}{e[a]\to e[a']}$$ Here $e[]$ is an evaluation context, "$a$" is an arbitrary term, and "$v$" is a value (which the author defines to be an abstraction -- variables, he says, are not values).
I am a bit confused. I think (but I'd need confirmation) that they are saying the same thing, but Rémy's approach actually allows for the specification of evaluation strategy (because I can then decide if the context hole will be to the left or to the right, etc), while the presentation by Hankin does not.
Is this correct, or did I completely miss the point?