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}
 
 \usepackage{hyperref}
 \usepackage{picins}
 

-\newcommand{\whelp}{Whelp}
-

 %\newcommand{\logo}[3]{
 %\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}}
 %}
 
 %\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{\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{\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{\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{\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
 
 \title{The proof assistant Matita}
 \author{Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi


@@ -47,13 +50,81 @@
 \section{Introduction}
 \label{sec:intro}
 
 \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
 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.
 
 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,
 \begin{thebibliography}{}
 
  \bibitem{annals} A.~Asperti, F.~Guidi, L.~Padovani, C.~Sacerdoti Coen,