From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 21 Mar 2006 09:00:58 +0000 (+0000)
Subject: done
X-Git-Tag: make_still_working~7488
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=da3ccf9b26b4b28c968b963d8718dbca4a4f5240;p=helm.git

done
---

diff --git a/helm/software/matita/tests/bool.ma b/helm/software/matita/tests/bool.ma
index 1b0952046..a49c21cc8 100644
--- a/helm/software/matita/tests/bool.ma
+++ b/helm/software/matita/tests/bool.ma
@@ -22,6 +22,8 @@ alias id "eq_ind" = "cic:/Coq/Init/Logic/eq_ind.con".
 alias id "eq_ind_r" = "cic:/Coq/Init/Logic/eq_ind_r.con".
 alias id "sym_eq" = "cic:/Coq/Init/Logic/sym_eq.con".
 
+(* 
+
 theorem SKK:
   \forall A:Set.
   \forall app: A \to A \to A.
@@ -643,3 +645,5 @@ theorem bool5:
     (inv (mult x y)) = (add (inv x) (inv y)).
 intros.auto paramodulation.
 qed.
+
+*)