X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Ftimes.ma;h=a36bd078c01877187072ee6fb804fd44beaacdaa;hb=2ecd65dbcc1388bb2dfe6425e6ef1b2e3f45c4ac;hp=c4e965fbf356f7e198a8e24f7d26d3767ad70700;hpb=5a702cea95883f7095c16b450e065ccb1714fc5a;p=helm.git

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index c4e965fbf..a36bd078c 100644
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -78,24 +78,24 @@ intros.elim x.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
     elim z.
       simplify.reflexivity.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
         apply lt_O_times_S_S.apply lt_O_times_S_S.
   elim y.
     simplify.reflexivity.
@@ -104,24 +104,24 @@ intros.elim x.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
     elim z.
       simplify.reflexivity.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
 qed.
 
@@ -134,8 +134,8 @@ eq nat (times (S n) (S (pred (minus (S p) (S q)))))
        (minus (pred (times (S n) (S p))) 
               (pred (times (S n) (S q)))).
 intros.
-rewrite < S_pred ? ?.  
-rewrite > minus_pred_pred ? ? ? ?.
+rewrite < S_pred.  
+rewrite > minus_pred_pred.
 rewrite < distr_times_minus. 
 reflexivity.  
 (* we now close all positivity conditions *)
@@ -151,7 +151,7 @@ intros.
 simplify. 
 change in match (plus p (times n (S p))) with (pred (times (S n) (S p))).
 change in match (plus q (times n (S q))) with (pred (times (S n) (S q))).
-rewrite < nat_compare_pred_pred ? ? ? ?.
+rewrite < nat_compare_pred_pred.
 rewrite < nat_compare_times_l.
 rewrite < nat_compare_S_S.
 apply nat_compare_elim p q.
@@ -236,4 +236,4 @@ qed.
 
 variant distr_Ztimes_Zplus: \forall x,y,z.
 eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)) \def
-distributive_Ztimes_Zplus.
\ No newline at end of file
+distributive_Ztimes_Zplus.