\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\pdftitle{ASCII Text}
\fixverbatim
\begin{popup}
\begin{verbatim*}
--------------------------- MODULE GCD ---------------------------
EXTENDS Integers, FiniteSets, TLAPS, NaturalsInduction

Divides(p, n) == \E q \in Int : n = p * q

DivisorsOf(n) == {p \in Int : Divides(p, n)}  

SetMax(S) ==  CHOOSE i \in S : \A j \in S : i >= j
  
GCD(m, n) == SetMax(DivisorsOf(m) \cap DivisorsOf(n)) 

THEOREM GCD1 == \A m \in Nat \ {0} : GCD(m, m) = m

THEOREM GCD2 == \A m, n \in Nat \ {0} : GCD(m, n) = GCD(n, m)

THEOREM GCD3 == \A m, n \in Nat \ {0} : 
                     (n > m) => (GCD(m, n) = GCD(m, n-m))
===================================================================
\end{verbatim*}
\end{popup}
\makeasciipopup