# HG changeset patch
# User wenzelm
# Date 754236953 -3600
# Node ID 0deb993885cee3a46d49115f75dac59144477b8f
# Parent  37025f8608a6f0f4ca9b49389a22927d33a02c63
corrected obvious errors;

diff -r 37025f8608a6 -r 0deb993885ce doc-src/Logics/CTT.tex
--- a/doc-src/Logics/CTT.tex	Thu Nov 25 14:43:42 1993 +0100
+++ b/doc-src/Logics/CTT.tex	Thu Nov 25 15:15:53 1993 +0100
@@ -64,7 +64,7 @@
 \begin{figure} \tabcolsep=1em  %wider spacing in tables
 \begin{center}
 \begin{tabular}{rrr} 
-  \it symbol    & \it meta-type         & \it description \\ 
+  \it name      & \it meta-type         & \it description \\ 
   \idx{Type}    & $t \to prop$          & judgement form \\
   \idx{Eqtype}  & $[t,t]\to prop$       & judgement form\\
   \idx{Elem}    & $[i, t]\to prop$      & judgement form\\
@@ -80,8 +80,8 @@
   \idx{Sum}     & $[t, i\to t]\to t$    & general sum type\\
   \idx{pair}    & $[i,i]\to i$          & constructor\\
   \idx{split}   & $[i,[i,i]\to i]\to i$ & eliminator\\
-  \idx{fst} snd & $i\to i$              & projections\\[2ex]
-  \idx{inl} inr & $i\to i$              & constructors for $+$\\
+  \idx{fst} \idx{snd} & $i\to i$        & projections\\[2ex]
+  \idx{inl} \idx{inr} & $i\to i$        & constructors for $+$\\
   \idx{when}    & $[i,i\to i, i\to i]\to i$    & eliminator for $+$\\[2ex]
   \idx{Eq}      & $[t,i,i]\to t$        & equality type\\
   \idx{eq}      & $i$                   & constructor\\[2ex]