From b8f0a76121fe684674c95fe9389b2e60b5eda694 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 30 Jan 2006 16:45:56 +0000
Subject: [PATCH] snapshot ...

---
 helm/papers/matita/matita.bib  | 10 +++++-----
 helm/papers/matita/matita2.bbl |  7 +++----
 helm/papers/matita/matita2.tex |  9 ++++-----
 3 files changed, 12 insertions(+), 14 deletions(-)

diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib
index 9e74514b7..5402461e4 100644
--- a/helm/papers/matita/matita.bib
+++ b/helm/papers/matita/matita.bib
@@ -463,8 +463,8 @@
 	    and Enrico Tassi and Stefano Zacchiroli",
   title =        "A content based mathematical search engine: Whelp",
   booktitle =    "Post-proceedings of the Types 2004 International Conference",
-  volume =       "LNCS, (to appear)",
-  pages =        "xxx--xxx",
+  volume =       "LNCS, 3839",
+  pages =        "17--32",
   publisher =    "Springer-Verlag",
   year =         "2004"
 }
@@ -971,7 +971,7 @@
 
 @misc{CoqManual,
  title = "The {C}oq Proof Assistant Reference Manual",
- author = "The Coq Development Team",
+ author = "{The Coq Development Team}",
  howpublished = "\\\url{http://coq.inria.fr/doc/main.html}",
  year = {2005},
  key = "CoqManual"
@@ -1069,7 +1069,7 @@
  howpublished = "W3C Recommendation 21 February 2001, \url{http://www.w3.org/TR/MathML2}",
  year = {2003},
  url = "\url{http://www.w3.org/TR/MathML2}",
- key = "Mathematical"
+ key = "MathML"
 }
 
 @misc{xml,
@@ -1078,7 +1078,7 @@ editor="{Tim Bray} and others",
  howpublished = "W3C Recommendation 10 February 1998,
                  \url{http://www.w3.org/TR/REC-xml}",
  url = "\url{http://www.w3.org/TR/REC-xml}",
- key = "Extensible"
+ key = "XML"
 }
 
 @misc{dom,
diff --git a/helm/papers/matita/matita2.bbl b/helm/papers/matita/matita2.bbl
index 3974d0107..936fd713d 100644
--- a/helm/papers/matita/matita2.bbl
+++ b/helm/papers/matita/matita2.bbl
@@ -10,7 +10,7 @@ Asperti, A., F. Guidi, L. Padovani, C. {Sacerdoti Coen}, and I. Schena: 2003,
 Asperti, A., F. Guidi, C. {Sacerdoti Coen}, E. Tassi, and S. Zacchiroli: 2004,
   `A content based mathematical search engine: Whelp'.
 \newblock In: {\em Post-proceedings of the Types 2004 International
-  Conference}, Vol. LNCS, (to appear). pp. xxx--xxx.
+  Conference}, Vol. LNCS, 3839. pp. 17--32.
 
 \bibitem{content-centric}
 Asperti, A., L. padovani, C. {Sacerdoti Coen}, and irene Schena: 2000,
@@ -65,8 +65,7 @@ Coscoy, Y., G. Kahn, and L. Thery: 1995, `{Extracting Text from Proofs}'.
   Informatique et en Automatique), France.
 
 \bibitem{mathml}
-Mathematical: 2003, `Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion
-  2.0'.
+MathML: 2003, `Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0'.
 \newblock W3C Recommendation 21 February 2001,
   \url{http://www.w3.org/TR/MathML2}.
 
@@ -100,7 +99,7 @@ Padovani, L.: 2003b, `On the Roles of LATEX and MathML in Encoding and
   of Mathematical Knowledge Management 2004}, Vol. LNCS, 3119. pp. 347--362.
 
 \bibitem{CoqManual}
-Team, T. C.~D.: 2005, `The {C}oq Proof Assistant Reference Manual'.
+{The Coq Development Team}: 2005, `The {C}oq Proof Assistant Reference Manual'.
 \newblock \\\url{http://coq.inria.fr/doc/main.html}.
 
 \bibitem{Werner}
diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 010d4713f..8745c56f0 100644
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -1400,7 +1400,7 @@ second searches the $\NT{wanted}$ term starting from these roots.
 %theorem valid_name: \forall n,m. m + n = n \to m = O.
 %  intros (n m H).
 %\end{grafite}
-%\noindent
+
 Consider the following sequent 
 \sequent{
 n:nat\\
@@ -1408,14 +1408,14 @@ m:nat\\
 H: m + n = n}{
 m=O
 }
-\noindent
+
 To change the right part of the equivalence of the $H$
 hypothesis with $O + n$ the user selects and pastes it as the pattern
 in the following statement.
 \begin{grafite}
   change in H:(? ? ? %) with (O + n).
 \end{grafite}
-\noindent
+
 To understand the pattern (or produce it by hand) the user should be
 aware that the notation $m+n=n$ hides the term $(eq~nat~(m+n)~n)$, so
 that the pattern selects only the third argument of $eq$.
@@ -1425,7 +1425,7 @@ to change at once all the occurrences of $n$ in the hypothesis $H$:
 \begin{grafite}
   change in H match n with (O + n).
 \end{grafite}
-\noindent
+
 In this case the $\NT{sequent\_path}$ selects the whole $H$, while
 the second phase locates $n$.
 
@@ -1434,7 +1434,6 @@ can automatically generate from the selection.
 \begin{grafite}
   change in H:(? ? (? ? %) %) with (O + n).
 \end{grafite}
-\noindent
 
 \subsubsection{Tactics supporting patterns}
 
-- 
2.39.5