X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FGround_2%2Fxoa_notation.ma;h=80f9762a67ea9fa77b2d2eb4dbbd6a0f959a61b4;hb=f75be90562ddd964ef7ed43b956eb908f3133e3a;hp=47e3268b413d24ebded3d547fa2af09cb50b5653;hpb=d6f1365a9f1cb48af8a7b32cf074373466779e7e;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma b/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma
index 47e3268b4..80f9762a6 100644
--- a/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma
@@ -156,3 +156,9 @@ notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2 break |
  non associative with precedence 30
  for @{ 'Or $P0 $P1 $P2 $P3 }.
 
+(* multiple conjunction connective (3) *)
+
+notation "hvbox(∧∧ term 34 P0 break & term 34 P1 break & term 34 P2)"
+ non associative with precedence 35
+ for @{ 'And $P0 $P1 $P2 }.
+