\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\pdftitle{ASCII Text}
\fixverbatim
\begin{popup}
\begin{verbatim*}
THEOREM Spec => []PartialCorrectness
<1>1. Init => Inv
<1>2. Inv /\ [Next]_vars => Inv'
<1>3. Inv => PartialCorrectness
<1>4. QED
\end{verbatim*}
\end{popup}
\makeasciipopup