\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\pdftitle{Creating a New Model in the Toolbox}
\file{create-new-model}
\makeindex
\begin{popup}
\subsection*{Creating a New Model in the Toolbox} 

\ctindex{1}{model!creating}{model-creating}%
On the \textsf{TLC Model Checker} menu, choose \textsf{New Model} and
enter any name you wish.  Then click \textsf{OK}.
\end{popup}
\makepopup