- added some cicbrowser screenshot (to be better placed in the text body)

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

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index ef4ebb1f3f23f61d9e9d1ddf640ef2f2dc88e2ed..2e3944bb5f68283ffc85a2f9e3d079d408c60167 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -63,6 +63,7 @@
 \newcommand{\NT}[1]{\ensuremath{\langle\mathit{#1}\rangle}}
 \newcommand{\URI}[1]{\texttt{#1}}
 \newcommand{\OP}[1]{``\texttt{#1}''}
+\newcommand{\SCRIPT}[1]{\texttt{#1}}
 
 \newenvironment{grafite}{\VerbatimEnvironment
  \begin{SaveVerbatim}{boxtmp}}%
@@ -127,8 +128,10 @@ Digital Libraries}
 
 \end{opening}
 
+% toc & co: to be removed in the final paper version
 \tableofcontents
 \listoffigures
+\listoftables
 
 \section{Introduction}
 \label{sec:intro}
@@ -298,7 +301,7 @@ allow other developers to quickly understand our code and contribute.
 
 \begin{figure}[!ht]
  \begin{center}
-  \includegraphics[width=0.9\textwidth,height=0.8\textheight]{libraries-clusters}
+  \includegraphics[width=0.9\textwidth,height=0.8\textheight]{pics/libraries-clusters}
   \caption[\MATITA{} components and related applications]{\MATITA{}
    components and related applications, with thousands of line of
    codes (klocs)}
@@ -1197,7 +1200,7 @@ fully supported so that mathematical glyphs can be input as such.
 
 \begin{figure}[!ht]
  \begin{center}
-  \includegraphics[width=0.95\textwidth]{matita-screenshot}
+  \includegraphics[width=0.95\textwidth]{pics/matita-screenshot}
   \caption{\MATITA{} look and feel}
   \label{fig:screenshot}
  \end{center}
@@ -1238,17 +1241,27 @@ latter it not a subterm. Once a meaningful (sub)term has been
 selected actions can be done on it like reductions or tactic
 applications.
 
-\begin{figure}[t]
+\begin{figure}[!ht]
  \begin{center}
-  \includegraphics[width=0.40\textwidth]{matita-screenshot-selection}
+  \includegraphics[width=0.40\textwidth]{pics/matita-screenshot-selection}
   \hspace{0.05\textwidth}
-  \raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{matita-screenshot-href}}
+  \raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{pics/matita-screenshot-href}}
   \caption{Semantic selection and hyperlinks}
   \label{fig:directmanip}
  \end{center}
 \end{figure}
 
-
+\begin{figure}[!ht]
+ \begin{center}
+  \includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-browsing}
+  \hspace{0.02\textwidth}
+  \includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-query}
+  \hspace{0.02\textwidth}
+  \includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-con}
+  \caption{Browsing and searching the library}
+  \label{fig:cicbrowser}
+ \end{center}
+\end{figure}
 
 \subsection{Patterns}
 
@@ -1665,25 +1678,27 @@ while, in the case of \COQ, \MATITA{} may only rely on XML files of
 The current library just comprises about one thousand theorems in 
 elementary aspects of arithmetics up to the multiplicative property for 
 Eulers' totient function $\phi$.
-The library is organized in five main directories: $logic$ (connectives,
-quantifiers, equality, $\dots$), $datatypes$ (basic datatypes and type 
-constructors), $nat$ (natural numbers), $Z$ (integers), $Q$ (rationals).
-The most complex development is $nat$, organized in 25 scripts, listed
-in Figure\ref{scripts}
-\begin{figure}[htb]
-$\begin{array}{lll}
-nat.ma    & plus.ma & times.ma  \\
-minus.ma  & exp.ma  & compare.ma \\
-orders.ma & le\_arith.ma &  lt\_arith.ma \\   
-factorial.ma & sigma\_and\_pi.ma & minimization.ma  \\
-div\_and\_mod.ma & gcd.ma & congruence.ma \\
-primes.ma & nth\_prime.ma & ord.ma\\
-count.ma  & relevant\_equations.ma & permutation.ma \\ 
-factorization.ma & chinese\_reminder.ma & fermat\_little\_th.ma \\     
-totient.ma& & \\
-\end{array}$
-\caption{\label{scripts}\MATITA{} scripts on natural numbers}
-\end{figure}
+The library is organized in five main directories: \texttt{logic} (connectives,
+quantifiers, equality, \ldots), \texttt{datatypes} (basic datatypes and type 
+constructors), \texttt{nat} (natural numbers), \texttt{Z} (integers), \texttt{Q}
+(rationals). The most complex development is \texttt{nat}, organized in 25
+scripts, listed in Tab.~\ref{tab:scripts}.
+
+\begin{table}[ht]
+ \begin{tabular}{lll}
+  \SCRIPT{nat.ma}    & \SCRIPT{plus.ma} & \SCRIPT{times.ma}  \\
+  \SCRIPT{minus.ma}  & \SCRIPT{exp.ma}  & \SCRIPT{compare.ma} \\
+  \SCRIPT{orders.ma} & \SCRIPT{le\_arith.ma} &  \SCRIPT{lt\_arith.ma} \\   
+  \SCRIPT{factorial.ma} & \SCRIPT{sigma\_and\_pi.ma} & \SCRIPT{minimization.ma}  \\
+  \SCRIPT{div\_and\_mod.ma} & \SCRIPT{gcd.ma} & \SCRIPT{congruence.ma} \\
+  \SCRIPT{primes.ma} & \SCRIPT{nth\_prime.ma} & \SCRIPT{ord.ma} \\
+  \SCRIPT{count.ma}  & \SCRIPT{relevant\_equations.ma} & \SCRIPT{permutation.ma} \\ 
+  \SCRIPT{factorization.ma} & \SCRIPT{chinese\_reminder.ma} &
+  \SCRIPT{fermat\_little\_th.ma} \\     
+  \SCRIPT{totient.ma} & & \\
+ \end{tabular}
+ \caption{\label{tab:scripts} Scripts on natural numbers in the standard library}
+\end{table}
 
 We do not plan to maintain the library in a centralized way, 
 as most of the systems do. On the contrary we are currently