X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Falpha_1%2Fsyntax%2Fterm_append.ma;h=a2db5fedd6cf1b23104a5fb0d0237dcc66c9df53;hp=4ea795a68d65fca1402cf8148e96abffa6eec155;hb=a77d0bd6a04e94f765d329d47b37d9e04d349b14;hpb=b598b37379baabef24ae511596be7f740cbb0c2e

diff --git a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma b/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma
index 4ea795a68..a2db5fedd 100644
--- a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma
+++ b/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma
@@ -22,4 +22,4 @@ let rec tappend T U on T ≝ match T with
 | TPair I V T ⇒ ②{I}V.(tappend T U)
 ].
 
-interpretation "append (term)" 'Append T U = (tappend T U).
+interpretation "append (term)" 'plus T U = (tappend T U).