X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita2.tex;h=fad520ad32b88fe42653294358e065ed3d67f57c;hb=804b1a97072cf1d1c76bc32338d0b068bcb2159f;hp=2cc1dc8a0af6b60067502a6838e1d049ff56da07;hpb=7a28be581787d98b13ffae6d3042261cde919d4f;p=helm.git

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 2cc1dc8a0..fad520ad3 100644
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -1287,9 +1287,9 @@ symmetric property for relations
 
 Then, you may state the symmetry of equality as
 \[ \forall A:Type. symmetric \;A\;(eq \; A)\]
-and \verb+symmetric_eq+ is valid Matita name fo such a theorem. 
+and \verb+symmetric_eq+ is valid Matita name for such a theorem. 
 So, somehow unexpectedly, the introduction of semi-rigid naming convention
-also had benefical effects on the global organization of the library, 
+has an important benefical effect on the global organization of the library, 
 forcing the user to define abstract notions and properties before 
 using them (and formalizing such use).
 
@@ -1313,11 +1313,11 @@ A typical example is the following
 \end{verbatim}
 where $eqb$ is boolean equality.
 In this cases, the name can be build starting from the matched
-expression and the suffix $_to_Prop$. In the above example, 
-$eqb_to_Prop$ is accepted. 
-
+expression and the suffix \verb+_to_Prop+. In the above example, 
+\verb+eqb_to_Prop+ is accepted. 
 
 
+\section{Conclusions}
 
 \acknowledgements
 We would like to thank all the students that during the past