-\documentclass[draft]{kluwer}
+\documentclass[]{kluwer}
\usepackage{color}
\usepackage{graphicx}
% \usepackage{amssymb,amsmath}
\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.
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
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).
\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