update in staic_2 and basic_2

[helm.git] / matita / matita / lib / lambda / background / notation.ma

diff --git a/matita/matita/lib/lambda/background/notation.ma b/matita/matita/lib/lambda/background/notation.ma
index 62b8b2dcadd3a974d1b4749e633e03a385bf3236..fdfffb346a035064fbf9755cc3acb1e475d2b3d5 100644 (file)
--- 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 }.