From 1cf49df11855525e05f65587be7198ecfdebc9e7 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 11 Apr 2001 15:36:03 +0000
Subject: coqweb

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1579 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/IntMap/Adist.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/IntMap/Adist.v b/theories/IntMap/Adist.v
index ec08fb35f1..f8bae6853c 100644
--- a/theories/IntMap/Adist.v
+++ b/theories/IntMap/Adist.v
@@ -258,10 +258,11 @@ Qed.
 (*s $d$ is an ultrametric distance, that is, not only $d(a,a')\leq d(a,a'')+d(a'',a')$,
   but in fact $d(a,a')\leq max(d(a,a''),d(a'',a'))$.
   This means that $min(pd(a,a''),pd(a'',a'))<=pd(a,a')$ (lemma [ad_pdist_ultra] below).
-  This follows from the fact that $a \Ra |a| = 1/2^\texttt{ad\_plength}(a))$
+  This follows from the fact that $a \Ra |a| = 1/2^{\texttt{ad\_plength}}(a))$
   is an ultrametric norm, i.e. that $|a-a'| \leq max (|a-a''|, |a''-a'|)$,
   or equivalently that $|a+b|<=max(|a|,|b|)$, i.e. that
-  min $(\texttt{ad\_plength}(a), \texttt{ad\_plength}(b)) \leq \texttt{ad\_plength} (a~\texttt{xor}~ b)$
+  min $(\texttt{ad\_plength}(a), \texttt{ad\_plength}(b)) \leq 
+  \texttt{ad\_plength} (a~\texttt{xor}~ b)$
   (lemma [ad_plength_ultra]).
 *)
 
-- 
cgit v1.2.3