Whatever versions of the Hahn-Banach theorems are presented in a book, what I've never seen left out is the extension lemma
Let $E$ be a real vector space, and $p \colon E \to \mathbb{R}$ a sublinear functional. If $M$ is a subspace of $E$, and $f\colon M \to \mathbb{R}$ a linear functional such that $f(x) \leqslant p(x)$ for all $x\in M$, then there exists a linear functional $F \colon E \to \mathbb{R}$ with $F\lvert_M = f$ and $F(x) \leqslant p(x)$ for all $x\in E$.
So I assume we can use that.
By definition, $B$ is $\sigma(X'',X')$-closed, and $x_0'' \notin B$. Since $\sigma(X'',X')$ is a vector space topology, there is a $\sigma(X'',X')$-neighbourhood $U$ of $0$ such that
$$B \cap (x_0'' + U + U) = \varnothing.\tag{1}$$
Rearranging $(1)$ yields $(B - U) \cap (x_0'' + U) = \varnothing$. Define $V := B - U$. Since $\sigma(X'',X')$ is locally convex, we can assume that $U$ is convex and balanced, and since $B$ is also convex and balanced, $V = B - U = B + U$ is then a convex and balanced $\sigma(X'',X')$-neighbourhood of $0$. In particular, $V$ is a convex and absorbant subset of $X''$. Its Minkowski functional
$$\mu_V \colon x \mapsto \inf \{ t > 0 : x \in t\cdot V\}$$
is then a sublinear functional on $X''$. Since $V$ is also balanced, $\mu_V$ is even a seminorm (but that plays no role, it's just an aside remark).
Now from $(x_0'' + U)\cap V = \varnothing$, it follows that $\mu_V(x_0'') > 1$. Let $M = \mathbb{R}\cdot x_0''$ and define $f\colon M \to \mathbb{R}$ by $f(\alpha \cdot x_0'') = \alpha\cdot \mu_V(x_0'')$.
By the lemma, there is a linear $F \colon X'' \to \mathbb{R}$ with $F(x_0'') = \mu_V(x_0'') > 1$ and $F(x'') \leqslant \mu_V(x'')$ for all $x'' \in X''$. Since clearly $\mu_V(x'') \leqslant 1$ for all $x'' \in V$, we can find $\alpha \in \bigl(1,\mu_V(x_0'')\bigr)$ and $\varepsilon > 0$ with
$$F(x'') \leqslant 1 < \alpha < \alpha + \varepsilon < \mu_V(x_0'') = F(x_0'').\tag{2}$$
In particular, we have $F(x) < \alpha$ for all $x\in B$.
It remains to see that $F$ is the evaluation functional for some $x'\in X'$. And that is equivalent to $F$ being $\sigma(X'',X')$-continuous. But by construction $F$ is bounded on some $\sigma(X'',X')$-neighbourhood of $0$ - namely $V$, or any smaller neighbourhood, like $U$ - and that implies $F$ is $\sigma(X'',X')$-continuous.
If Conway proves the separation theorem for locally convex spaces [the above is essentially a proof of that, a few details need to be generalised], we can simply invoke that for the space $(X'',\sigma(X'',X'))$, since by construction $B$ is a $\sigma(X'',X')$-closed convex set, and $\{x_0''\}$ is a $\sigma(X'',X')$-compact convex set disjoint from $B$.