Minor changes.

[helm.git] / helm / papers / matita / matita2.tex

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 2cc1dc8a0af6b60067502a6838e1d049ff56da07..fad520ad32b88fe42653294358e065ed3d67f57c 100644 (file)
--- 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)\]
 
 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
 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).
 
 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
 \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
 
 \acknowledgements
 We would like to thank all the students that during the past