X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fbool.ma;h=a49c21cc82763a4ca6a5b3ab8f45b70b048dcb31;hb=da3ccf9b26b4b28c968b963d8718dbca4a4f5240;hp=1b095204629781cda43c51e4677ff7ef65f5de0f;hpb=c6c735136c2fe236c6b7284e7b768d87c96a4537;p=helm.git

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.
+
+*)