bumped year

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

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 2cc1dc8a0af6b60067502a6838e1d049ff56da07..c5c0fff05b9e433c444bd921cf1ed71982c5904f 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -1,4 +1,4 @@
-\documentclass[draft]{kluwer}
+\documentclass[]{kluwer}

 \usepackage{color}
 \usepackage{graphicx}
 % \usepackage{amssymb,amsmath}
 \usepackage{color}
 \usepackage{graphicx}
 % \usepackage{amssymb,amsmath}


@@ -270,6 +270,14 @@ allow other developers to quickly understand our code and contribute.
  \end{center}
 \end{figure}
 
  \end{center}
 \end{figure}
 

+\begin{figure}[t]
+ \begin{center}
+  \includegraphics[width=0.9\textwidth]{libraries.ps}
+  \caption{\MATITA{} libraries}
+  \label{fig:libraries}
+ \end{center}
+\end{figure}
+

 \section{Overview of the Architecture}
 Fig.~\ref{fig:libraries} shows the architecture of the \emph{libraries} (circle nodes)
 and \emph{applications} (squared nodes) developed in the HELM project.
 \section{Overview of the Architecture}
 Fig.~\ref{fig:libraries} shows the architecture of the \emph{libraries} (circle nodes)
 and \emph{applications} (squared nodes) developed in the HELM project.


@@ -1252,7 +1260,7 @@ development of the library, encouraging people to expand,
 modify and elaborate previous contributions.
 
 \subsection{Matita's naming convention}
 modify and elaborate previous contributions.
 
 \subsection{Matita's naming convention}

-A minor but not entirely negligeable aspect of Matita is that of
+A minor but not entirely negligible aspect of Matita is that of

 adopting a (semi)-rigid naming convention for identifiers, derived by 
 our studies about metadata for statements. 
 The convention is only applied to identifiers for theorems 
 adopting a (semi)-rigid naming convention for identifiers, derived by 
 our studies about metadata for statements. 
 The convention is only applied to identifiers for theorems 


@@ -1287,9 +1295,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,17 +1321,17 @@ 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
 five years collaborated in the \HELM{} project and contributed to 
 the development of Matita, and in particular
 
 \acknowledgements
 We would like to thank all the students that during the past
 five years collaborated in the \HELM{} project and contributed to 
 the development of Matita, and in particular

-A.~Griggio, F.~Guidi, P.~Di~Lena, L.~Padovani, I.~Schena, M.~Selmi, 
+M.~Galat\`a, A.~Griggio, F.~Guidi, P.~Di~Lena, L.~Padovani, I.~Schena, M.~Selmi,

 and V.~Tamburrelli.
 
 \theendnotes
 and V.~Tamburrelli.
 
 \theendnotes