- contex-free normal forms started

[helm.git] / matita / matita / contribs / lambda_delta / Ground_2 / xoa_notation.ma

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 47e3268b413d24ebded3d547fa2af09cb50b5653..80f9762a67ea9fa77b2d2eb4dbbd6a0f959a61b4 100644 (file)
--- 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 }.
+