Snapshot

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

diff --git a/helm/papers/matita/matita2.bbl b/helm/papers/matita/matita2.bbl
index b407a8286781e480f1c3ab34650c9526dd82614d..9ccdd2e07bb8c0e8f63584afc43e6d0e99730e65 100644 (file)
--- a/helm/papers/matita/matita2.bbl
+++ b/helm/papers/matita/matita2.bbl
@@ -81,6 +81,11 @@ Coscoy, Y., G. Kahn, and L. Thery: 1995, `{Extracting Text from Proofs}'.
 \newblock Technical Report RR-2459, Inria (Institut National de Recherche en
   Informatique et en Automatique), France.
 
+\bibitem{delahaye}
+Delahaye, D. and R. di~Cosmo: 1999, `Information Retrieval in a {C}oq Proof
+  Library using Type Isomorphisms'.
+\newblock In: {\em Proceedings of TYPES 99}, Vol. LNCS.
+
 \bibitem{geuvers-jojgov}
 Geuvers, H. and G.~I. Jojgov: 2002, `Open Proofs and Open Terms: A Basis for
   Interactive Logic'.
@@ -113,9 +118,9 @@ Nieuwenhuis, R. and A. Rubio: 2001, {\em Paramodulation-based thorem proving}.
 \newblock ISBN-0-262-18223-8.
 
 \bibitem{omdoc}
-OMDoc: 2005, `{OMDoc}: An Open Markup Format for Mathematical Documents
-  (Version 1.1)'.
-\newblock \\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.1.pdf}.
+OMDoc: 2005, `{OMDoc}: An Open Markup Format for Mathematical Documents (Draft,
+  Version 1.2)'.
+\newblock \\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.2.pdf}.
 
 \bibitem{padovani}
 Padovani, L.: 2003a, `MathML Formatting'.