update in ground_2 + \lambda\delta-related ignores

diff --git a/.gitignore b/.gitignore
index af77f87fa263227320df6a75f6ea4d7137250ae4..a433c4179b22556d421c4e107fefea6b08fc06fd 100644 (file)
--- a/.gitignore
+++ b/.gitignore
@@ -38,3 +38,5 @@ matita/matita/contribs/lambdadelta/token
 matita/matita/contribs/lambdadelta/2A1
 matita/matita/contribs/lambdadelta/apps_2/notation
 matita/matita/contribs/lambdadelta/apps_2/models
+matita/matita/contribs/lambdadelta/ground_2/xoa/xoa2.ma
+matita/matita/contribs/lambdadelta/ground_2/notation/xoa/notation2.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma
index 408e1933dec9e3c55744a695c6c63f6a22e8238e..530c0e2b39541f81f971847c667b4f317a41a108 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma
@@ -22,3 +22,9 @@ include "ground_2/xoa/xoa.ma".
 interpretation "logical false" 'false = False.
 
 interpretation "logical true" 'true = True.
+
+(* Logical properties missing in the basic library **************************) 
+
+lemma commutative_and: ∀A,B. A ∧ B → B ∧ A.
+#A #B * /2 width=1 by conj/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml
index 593d918735af0155cd9bdf77ec2c7ae58bd658f4..27e0709039e19d1bf298ae7d7c407f258d900065 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml
+++ b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml
@@ -5,5 +5,6 @@
     <key name="objects">ground_2/xoa/xoa2</key>
     <key name="notations">ground_2/notation/xoa/notation2</key>
     <key name="include">basics/pts.ma</key>
+    <key name="ex">3 6</key>
   </section>
 </helm_registry>