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