From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 1 Feb 2006 23:12:00 +0000 (+0000)
Subject: line breaking
X-Git-Tag: make_still_working~7693
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=951069678fea0d6dcdde984320ec5057ddc57c3c;p=helm.git

line breaking
---

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index d902d1380..a0c014251 100644
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -1578,7 +1578,8 @@ where \texttt{H} is $\beta$-expanded over the second \texttt{n}
 occurrence. 
 
 At this point, since \COQ{} unification algorithm is essentially first-order,
-the application of an elimination principle (a term with type $\forall P.\forall
+the application of an elimination principle (a term of type\linebreak
+$\forall P.\forall
 x.(H~x)\to (P~x)$) will unify \texttt{x} with \texttt{n} and \texttt{P} with
 \texttt{(fun n0: nat => m + n = n0)}.