In the reference you posted there is a link to an online version of the monograph by S.Basu, M.-F.Roy, and R.Pollack, where algorithms like this are described (cf. Sect. 10.4, Algorithm 10.15).
The technique there is very general, and applies to non-Archimedean real closed fields, e.g. to fields of Puseaux series w.r.t. to an infinitesimal. There you don't have anything like "numeric evaluation".
Having said this, I wonder whether Thom encoding is really better for the range of problems like "straight" arbitrary precision computations with algebraic reals. For the latter, isolating roots by rational numbers works as well, and is faster, in theory, according to the reference.
Thom encodings really shine when one has a parametric (e.g. multivariate), or/and a non-Archimedean, setting.
Computation with isolating intervals is implemented e.g. in Sage.
sage: s=sqrt(AA(2))
sage: s.numerical_approx(prec=1000)
1.4142135623730950488016887242096980785696718753769480731766797379907324784...
sage: s>AA(0)
True
sage: t=s-sqrt(AA(3))
sage: t.minpoly()
x^4 - 10*x^2 + 1
sage: t.sign()
-1
