\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\makeindex
\file{zenon-isabelle}
\pdftitle{Zenon and Isabelle}
\begin{popup}
  \ctindex{2}{Zenon@\mmath{Zenon} (backend prover)}{Zenon}%
  \ctindex{2}{Isabelle@\mmath{Isabelle} (backend prover)}{Isabelle}%
  \ctindex{1}{Doligez, Damien}{doligez-damien}%
  \ctindex{1}{Paulson, Lawrence}{paulson}%
  \ctindex{1}{Merz, Stephan}{merz}%
  \vspace{-2\baselineskip}%
\subsection*{Zenon and Isabelle} \emph{Zenon} is a prover implemented
by Damien Doligez.  \emph{Isabelle} is a prover designed and
originally implemented by Lawrence Paulson.  TLAPS calls
\emph{Isabelle} with a special \tlaplus\ theory implemented primarily
by Stephan Merz.  Whenever \emph{Isabelle is} mentioned in this
hyperbook, it really means \emph{Isabelle}/\tlaplus, the
\emph{Isabelle} prover run with the \tlaplus\ theory.
\end{popup}
\makepopup