X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fcore_notation.ma;h=3f6eda5a78fb41e7ec58daf35fd585ca71c36ae4;hb=723514507b1e2e58c0a8c7bcc39c5d1301b910bc;hp=904adcd52f2fff140dd65eadb6e0945a219c4237;hpb=d2b59bd89f761a16a2dbc663f446b4f95c767b83;p=helm.git

diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma
index 904adcd52..3f6eda5a7 100644
--- a/matita/matita/lib/basics/core_notation.ma
+++ b/matita/matita/lib/basics/core_notation.ma
@@ -27,6 +27,14 @@ notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
           @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
        }.
 
+notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'exists2 (λ${ident x0}.$P0) (λ${ident x0}.$P1) }.
+
+notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'exists2 (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) }.
+
 (* sigma ********************************************************************)
 
 notation < "hvbox(\Sigma ident i : ty break . p)"
@@ -249,10 +257,10 @@ for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
 notation > "hvbox({ ident i | term 19 p })" with precedence 90
 for @{ 'subset (\lambda ${ident i}. $p)}.
 
-notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+notation < "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90
 for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
 
-notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+notation > "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90
 for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
 
 notation "hvbox(a break ∈ b)" non associative with precedence 45