minor fixes (-nodb works again)

[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}
@@ -270,6 +270,14 @@ allow other developers to quickly understand our code and contribute.
  \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.
@@ -1252,7 +1260,7 @@ development of the library, encouraging people to expand,
 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 
@@ -1287,9 +1295,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,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
-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
-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