doc-src/Logics/CTT.tex

--- a/doc-src/Logics/CTT.tex	Wed May 07 17:16:18 1997 +0200
+++ b/doc-src/Logics/CTT.tex	Wed May 07 17:16:36 1997 +0200
@@ -669,7 +669,6 @@
 \tdx{div_def}           a div b ==
                   rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y.v))
 
-
 \tdx{add_typing}        [| a:N;  b:N |] ==> a #+ b : N
 \tdx{addC0}             b:N ==> 0 #+ b = b : N
 \tdx{addC_succ}         [| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N