From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 6 Dec 2005 11:57:34 +0000 (+0000)
Subject: Minor changes.
X-Git-Tag: make_still_working~8041
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=804b1a97072cf1d1c76bc32338d0b068bcb2159f;p=helm.git

Minor changes.
---

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