X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Fbackground%2Fnotation.ma;h=fdfffb346a035064fbf9755cc3acb1e475d2b3d5;hb=647504aa72b84eb49be8177b88a9254174e84d4b;hp=62b8b2dcadd3a974d1b4749e633e03a385bf3236;hpb=aa9654656f7d0aeb9345e0b86a9e35f861687580;p=helm.git

diff --git a/matita/matita/lib/lambda/background/notation.ma b/matita/matita/lib/lambda/background/notation.ma
index 62b8b2dca..fdfffb346 100644
--- a/matita/matita/lib/lambda/background/notation.ma
+++ b/matita/matita/lib/lambda/background/notation.ma
@@ -37,14 +37,18 @@ notation "hvbox( { term 46 b } # break term 90 i )"
  non associative with precedence 46
  for @{ 'VariableReferenceByIndex $b $i }.
 
-notation "hvbox( 𝛌  . term 46 A )"
+notation "hvbox( 𝛌 . term 46 A )"
    non associative with precedence 46
    for @{ 'Abstraction $A }.
 
-notation "hvbox( { term 46 b } 𝛌  . break term 46 T)"
+notation "hvbox( { term 46 b } 𝛌 . break term 46 T)"
    non associative with precedence 46
    for @{ 'Abstraction $b $T }.
 
+notation "hvbox( 𝛌 term 46 d . break term 46 A )"
+   non associative with precedence 46
+   for @{ 'AnnotatedAbstraction $d $A }.
+
 notation "hvbox( @ term 46 C . break term 46 A )"
    non associative with precedence 46
    for @{ 'Application $C $A }.