From 03f843e53f48f6bc363656060a31bb29c4e0be38 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 10 Oct 2006 13:12:44 +0000 Subject: [PATCH] auto => auto new --- matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma b/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma index 6773470b0..be5f789a3 100644 --- a/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma +++ b/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. *) -- 2.39.2