X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fcomputation%2Fcsn_cprs.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fcomputation%2Fcsn_cprs.ma;h=4a936f607864a36067ed488aa7b4bdc18ea1ebdb;hb=fcd30dfead2fbc2889aa993fba0577dce8a90c88;hp=ace3b9feab2764fcb41615cc2508e783744b46d2;hpb=6d31022dd760f9cb9121d1ed9377d6bceac7ac22;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cprs.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cprs.ma
index ace3b9fea..4a936f607 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cprs.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cprs.ma
@@ -25,10 +25,6 @@ interpretation
    "context-sensitive strong normalization (term)"
    'SNStar L T = (csns L T).
 
-notation "hvbox( L ⊢ ⬇ * * T )"
-   non associative with precedence 45
-   for @{ 'SNStar $L $T }.
-
 (* Basic eliminators ********************************************************)
 
 lemma csns_ind: ∀L. ∀R:predicate term.