1.1 --- a/doc-src/Logics/CTT.tex	Fri May 02 16:18:11 1997 +0200
     1.2 +++ b/doc-src/Logics/CTT.tex	Fri May 02 16:18:49 1997 +0200
     1.3 @@ -696,7 +696,7 @@
     1.4  \tdx{diff_succ_succ}    [| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N
     1.5  \tdx{diff_self_eq_0}    a:N ==> a - a = 0 : N
     1.6  \tdx{add_inverse_diff}  [| a:N;  b:N;  b-a=0 : N |] ==> b #+ (a-b) = a : N
     1.7 -\caption{The theory of arithmetic} \label{ctt-arith}
     1.8 +\caption{The theory of arithmetic} \label{ctt_arith}
     1.9  \end{ttbox}
    1.10  \end{figure}
    1.11  
    1.12 @@ -706,7 +706,7 @@
    1.13  properties of addition, multiplication, subtraction, division, and
    1.14  remainder, culminating in the theorem
    1.15  \[ a \bmod b + (a/b)\times b = a. \]
    1.16 -Figure~\ref{ctt-arith} presents the definitions and some of the key
    1.17 +Figure~\ref{ctt_arith} presents the definitions and some of the key
    1.18  theorems, including commutative, distributive, and associative laws.
    1.19  
    1.20  The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'mod'