X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Flimits%2Fclass_eq.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Flimits%2Fclass_eq.ma;h=0000000000000000000000000000000000000000;hb=700b170aa9b0377d33f1edd44de8d89129477fb8;hp=b86e5f2961f79d60ef75010320b10aab72820feb;hpb=d7f32114f3806b51c2ee483dcb5a86e08d086a72;p=helm.git

diff --git a/helm/software/matita/contribs/limits/class_eq.ma b/helm/software/matita/contribs/limits/class_eq.ma
deleted file mode 100644
index b86e5f296..000000000
--- a/helm/software/matita/contribs/limits/class_eq.ma
+++ /dev/null
@@ -1,32 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* STATO: NON COMPILA: dev'essere aggiornato *)
-
-set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_eq".
-
-include "class_defs.ma".
-
-theorem ceq_trans: \forall C. \xforall c1,c2. ceq C c1 c2 \to 
-                   \xforall c3. ceq ? c2 c3 \to ceq ? c1 c3.
-intros.
-
-(*
-apply ceq_intro; apply cle_trans; [|auto new timeout=100|auto new timeout=100||auto new timeout=100|auto new timeout=100].
-qed.
-
-theorem ceq_sym: \forall C,c1,c2. ceq C c1 c2 \to ceq C c2 c1.
-intros; elim H; clear H.; auto new timeout=100.
-qed.
-*)