doc-src/Logics/CTT.tex
 changeset 3096 ccc2c92bb232 parent 975 6c280d1dac35 child 3133 8c55b0f16da2
--- 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'