paper skeleton

diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex
index d6dae46e74b3d26052a1c08a1cac909a019da4e3..d0817571912d4084148560dd46b05be2dde1804b 100644 (file)
--- a/helm/papers/matita/matita.tex
+++ b/helm/papers/matita/matita.tex
@@ -5,31 +5,34 @@
 \usepackage{hyperref}
 \usepackage{picins}
 
-\newcommand{\whelp}{Whelp}
-
 %\newcommand{\logo}[3]{
 %\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}}
 %}
 
-\newcommand{\coq}{Coq}
-\newcommand{\mowgli}{MoWGLI}
-\newcommand{\IR}{\ensuremath{\mathbb{R}}}
+\newcommand{\AUTO}{\textsc{Auto}}
+\newcommand{\COQ}{Coq}
+\newcommand{\ELIM}{\textsc{Elim}}
+\newcommand{\HELM}{Helm}
+\newcommand{\HINT}{\textsc{Hint}}
 \newcommand{\IN}{\ensuremath{\mathbb{N}}}
-\newcommand{\instance}{\textsc{Instance}}
-\newcommand{\auto}{\textsc{Auto}}
-\newcommand{\hint}{\textsc{Hint}}
-\newcommand{\locate}{\textsc{Locate}}
-\newcommand{\elim}{\textsc{Elim}}
-\newcommand{\match}{\textsc{Match}}
-\newcommand{\texmacro}[1]{\texttt{\char92 #1}}
-\newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
-\newcommand{\NAT}{\ensuremath{\mathit{nat}}}
-\newcommand{\Prop}{\mathit{Prop}}
-\newcommand{\natind}{\mathit{nat\_ind}}
-\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
+\newcommand{\INSTANCE}{\textsc{Instance}}
+\newcommand{\IR}{\ensuremath{\mathbb{R}}}
 \newcommand{\LIBXSLT}{LibXSLT}
+\newcommand{\LOCATE}{\textsc{Locate}}
+\newcommand{\MATCH}{\textsc{Match}}
+\newcommand{\MATITA}{Matita}
+\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
+\newcommand{\MOWGLI}{MoWGLI}
+\newcommand{\NAT}{\ensuremath{\mathit{nat}}}
+\newcommand{\NATIND}{\mathit{nat\_ind}}
 \newcommand{\OCAML}{OCaml}
+\newcommand{\PROP}{\mathit{Prop}}
+\newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
+\newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
 \newcommand{\UWOBO}{UWOBO}
+\newcommand{\WHELP}{Whelp}
+
+\newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
 
 \title{The proof assistant Matita}
 \author{Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi
@@ -47,13 +50,81 @@
 \section{Introduction}
 \label{sec:intro}
 
-{\bf Acknowledgements}
+\begin{itemize}
+ \item scelta del sistema fondazionale
+ \item sistema indipendente (da Coq)
+  \begin{itemize}
+   \item possibilit\`a di sperimentare (soluzioni architetturali, logiche,
+    implementative, \dots)
+   \item compatibilit\`a con sistemi legacy
+  \end{itemize}
+\end{itemize}
+
+\textbf{Acknowledgements}
 We would like to thank all the students that during the past
-five years collaborated in the Helm project and contributed to 
+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, 
 V.Tamburrelli.
 
+\section{Features}
+
+\subsection{mathml}
+\ASSIGNEDTO{zack}
+
+\subsection{metavariabili}
+\ASSIGNEDTO{csc}
+
+\subsection{pattern}
+\ASSIGNEDTO{gares}
+
+\subsection{tatticali}
+\ASSIGNEDTO{gares}
+
+\subsection{disambiguazione}
+\ASSIGNEDTO{zack}
+
+\subsection{notazione}
+\ASSIGNEDTO{zack}
+
+\subsection{libreria tutta visibile}
+\ASSIGNEDTO{csc}
+
+\subsection{ricerca e indicizzazione}
+\ASSIGNEDTO{andrea}
+
+\subsection{auto}
+\ASSIGNEDTO{andrea}
+
+\subsection{xml / gestione della libreria}
+\ASSIGNEDTO{gares}
+
+\subsection{named variable}
+\ASSIGNEDTO{csc}
+
+\subsection{assenza di proof tree / resa in linguaggio naturale}
+\ASSIGNEDTO{andrea}
+
+\subsection{selezione semantica, cut paste, hyperlink}
+\ASSIGNEDTO{zack}
+
+\subsection{sostituzioni esplicite vs moduli}
+\ASSIGNEDTO{csc}
+
+\section{Drawbacks, missing, \dots}
+
+\subsection{moduli}
+\ASSIGNEDTO{}
+
+\subsection{ltac}
+\ASSIGNEDTO{}
+
+\subsection{estrazione}
+\ASSIGNEDTO{}
+
+\subsection{localizzazione errori}
+\ASSIGNEDTO{}
+
 \begin{thebibliography}{}
 
  \bibitem{annals} A.~Asperti, F.~Guidi, L.~Padovani, C.~Sacerdoti Coen,