From: Enrico Tassi Date: Tue, 21 Mar 2006 09:00:58 +0000 (+0000) Subject: done X-Git-Tag: 0.4.95@7852~1586 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fb3ae649cf1079117166318809ac5a2dba987dcd;p=helm.git done --- diff --git a/matita/tests/bool.ma b/matita/tests/bool.ma index 1b0952046..a49c21cc8 100644 --- a/matita/tests/bool.ma +++ b/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. + +*)