\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\makeindex
\pdftitle{Running TLC}
\file{run-tlc}
\begin{popup}
  \tindex{1}{running TLC model checker}%
  \ctindex{1}{TLC!running}{tlc-running}%
  \vspace{-2\baselineskip}
\subsection*{Running TLC} 

To run TLC, click on the green arrow button
\raisebox{-2pt}{\scalebox{.625}{\includegraphics{tlc-run-button.jpg}}}
near the top of the window.  You can also run TLC by selecting
\textsf{Run model} from the \textsf{TLC Model Checker} menu, or by
typing (the single key named) \textsf{F11}.
\end{popup}
\makepopup