milestone update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / lib / list.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list.ma b/matita/matita/contribs/lambdadelta/ground/lib/list.ma
index 781fc27a55791dde08660777837f20b879e9892e..184438f613ecab4600a4865934ae2d1384194890 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/list.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list.ma
@@ -31,8 +31,7 @@ interpretation
   "cons (lists)"
   'OPlusRight A hd tl = (list_cons A hd tl).
 
-rec definition list_all A (R:predicate A) (l:list A) on l ≝
-match l with
+rec definition list_all A (R:predicate A) (l:list A) on l ≝ match l with
 [ list_nil        ⇒ ⊤
 | list_cons hd tl ⇒ ∧∧ R hd & list_all A R tl
 ].