- transcript: patched to generate CoRN_notation.ma instead of CoRN.ma

[helm.git] / matita / contribs / PREDICATIVE-TOPOLOGY / class_eq.ma

diff --git a/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma b/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
index 7634cbde1171f65fa92d126eea1c8a872fc2f971..b86e5f2961f79d60ef75010320b10aab72820feb 100644 (file)
--- a/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
+++ b/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* STATO: NON COMPILA: dev'essere aggiornato *)
+
 set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_eq".
 
 include "class_defs.ma".
@@ -21,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 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.
+intros; elim H; clear H.; auto new timeout=100.
 qed.
-*)
\ No newline at end of file
+*)