X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Fcompare.ma;h=4a5025975fe3d8d4b3f610563b565dce39be6bac;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=a59100885e791d8ba504fc07e970d57266bcb920;hpb=fb94e5a71be508516514dfe50528ccfb3cd2da91;p=helm.git

diff --git a/helm/matita/library/Z/compare.ma b/helm/matita/library/Z/compare.ma
index a59100885..4a5025975 100644
--- a/helm/matita/library/Z/compare.ma
+++ b/helm/matita/library/Z/compare.ma
@@ -49,17 +49,17 @@ elim x.
     simplify.apply not_eq_OZ_pos.
     simplify.apply not_eq_OZ_neg.
   elim y.
-    simplify.intro.apply (not_eq_OZ_pos n).apply sym_eq.assumption.
+    simplify.unfold Not.intro.apply (not_eq_OZ_pos n).apply sym_eq.assumption.
     simplify.apply eqb_elim.
       intro.simplify.apply eq_f.assumption.
-      intro.simplify.intro.apply H.apply inj_pos.assumption.
+      intro.simplify.unfold Not.intro.apply H.apply inj_pos.assumption.
     simplify.apply not_eq_pos_neg.
   elim y.
-    simplify.intro.apply (not_eq_OZ_neg n).apply sym_eq.assumption.
-    simplify.intro.apply (not_eq_pos_neg n1 n).apply sym_eq.assumption.
+    simplify.unfold Not.intro.apply (not_eq_OZ_neg n).apply sym_eq.assumption.
+    simplify.unfold Not.intro.apply (not_eq_pos_neg n1 n).apply sym_eq.assumption.
     simplify.apply eqb_elim.
       intro.simplify.apply eq_f.assumption.
-      intro.simplify.intro.apply H.apply inj_neg.assumption.
+      intro.simplify.unfold Not.intro.apply H.apply inj_neg.assumption.
 qed.
 
 theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.