Typos.

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index 9a1f4ec25f442d05dc5d707b14f80db3bbe44572..a654029110b80f0b0db5e4f03662e06d571413d5 100644 (file)
--- a/helm/papers/system_T/t.tex
+++ b/helm/papers/system_T/t.tex
@@ -28,7 +28,7 @@
 \section{Introduction}
 The characterization of the provable recursive functions of 
 Peano Arithmetic as the terms of system T is a well known
-result of G\"odel \cite{Godel58,Godel90}. Although many authors acknowledge 
+result of G\"odel \cite{Godel58,Godel90}. Although several authors acknowledge 
 that the functional interpretation of the Dialectica paper
 is not among the major achievements of the author (see e.g. \cite{Girard87}), 
 the result has been extensively investigated and there is a wide 
@@ -62,7 +62,7 @@ prefer to focus on higher order arithmetics and its relation with
 Girard's System $F$ \cite{Girard86}, but the technical complexity and
 the didactical value of the two proofs is not comparable: when you 
 prove that the Induction Principle is realized by the recursor $R$ 
-of system $T$ you catch a sudden gleam of intelligence in the 
+of system $T$ you catch a sudden gleam of understanding in the 
 students eyes; usually, the same does not happen when you show, say, 
 that the ``forgetful'' intrepretation of the higher order predicate defining
 the natural numbers is the system $F$ encoding