From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 10 Oct 2006 13:12:44 +0000 (+0000)
Subject: auto => auto new
X-Git-Tag: make_still_working~6769
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5b8cff10c1c13376ec0f36ecc72ed8c6524b0310;p=helm.git

auto => auto new
---

diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
index 6773470b0..be5f789a3 100644
--- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
+++ b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
@@ -23,10 +23,10 @@ theorem ceq_trans: \forall C. \xforall c1,c2. ceq C c1 c2 \to
 intros.
 
 (*
-apply ceq_intro; apply cle_trans; [|auto|auto||auto|auto].
+apply ceq_intro; apply cle_trans; [|auto new|auto new||auto new|auto new].
 qed.
 
 theorem ceq_sym: \forall C,c1,c2. ceq C c1 c2 \to ceq C c2 c1.
-intros; elim H; clear H.; auto.
+intros; elim H; clear H.; auto new.
 qed.
 *)