X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fground_2%2Fxoa_notation.ma;h=ed4b83f83cb25a970106b7428d0c47f622e27a75;hb=53f874fba5b9c39a788085515a4fefe5d29281da;hp=8a167c86ae5a8a0f3df54caccdf9b5edb9ae1465;hpb=a2144f09d1bd7022c1f2dfd4909a1fb9772c8d56;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 8a167c86a..ed4b83f83 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma
@@ -252,3 +252,9 @@ notation "hvbox(∧∧ term 34 P0 break & term 34 P1 break & term 34 P2)"
  non associative with precedence 35
  for @{ 'And $P0 $P1 $P2 }.
 
+(* multiple conjunction connective (4) *)
+
+notation "hvbox(∧∧ term 34 P0 break & term 34 P1 break & term 34 P2 break & term 34 P3)"
+ non associative with precedence 35
+ for @{ 'And $P0 $P1 $P2 $P3 }.
+