Removed final question marks from {apply|elim|rewrite}s.

(This used to change the goals order, but it has now been fixed by Gares)

diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma
index 4878078fc44482f8ed80b3d138c27d7ba9446726..1ff2adcd8dfa0bf99462486ce3641519849e0df7 100644 (file)
--- a/helm/matita/library/Q/q.ma
+++ b/helm/matita/library/Q/q.ma
@@ -162,13 +162,13 @@ apply fraction_elim2 (\lambda f,g. Or (f=g) (f=g \to False)).
     right.apply not_eq_pp_nn.
     right.apply not_eq_pp_cons.
   intros. elim g1.
     right.apply not_eq_pp_nn.
     right.apply not_eq_pp_cons.
   intros. elim g1.

-      right.intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption.
+      right.intro.apply not_eq_pp_nn n1 n.apply sym_eq. assumption.

       elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)).
         left. apply eq_f. assumption.
         right.intro.apply H.apply injective_nn.assumption.
       right.apply not_eq_nn_cons.
       elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)).
         left. apply eq_f. assumption.
         right.intro.apply H.apply injective_nn.assumption.
       right.apply not_eq_nn_cons.

-  intros.right.intro.apply not_eq_pp_cons m x f1 ?.apply sym_eq.assumption.
-  intros.right.intro.apply not_eq_nn_cons m x f1 ?.apply sym_eq.assumption.
+  intros.right.intro.apply not_eq_pp_cons m x f1.apply sym_eq.assumption.
+  intros.right.intro.apply not_eq_nn_cons m x f1.apply sym_eq.assumption.

   intros.elim H.
     elim ((decidable_eq_Z x y) : Or (x=y) (x=y \to False)).
       left.apply eq_f2.assumption.
   intros.elim H.
     elim ((decidable_eq_Z x y) : Or (x=y) (x=y \to False)).
       left.apply eq_f2.assumption.


@@ -192,12 +192,12 @@ intros.apply fraction_elim2
     simplify.apply not_eq_pp_nn.
     simplify.apply not_eq_pp_cons.
   intros.elim g1.
     simplify.apply not_eq_pp_nn.
     simplify.apply not_eq_pp_cons.
   intros.elim g1.

-    simplify.intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption.
+    simplify.intro.apply not_eq_pp_nn n1 n.apply sym_eq. assumption.

     simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
     intro.simplify.intro.apply H.apply injective_nn.assumption.
   simplify.apply not_eq_nn_cons.
     simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
     intro.simplify.intro.apply H.apply injective_nn.assumption.
   simplify.apply not_eq_nn_cons.

-  intros.simplify.intro.apply not_eq_pp_cons m x f1 ?.apply sym_eq. assumption.
-  intros.simplify.intro.apply not_eq_nn_cons m x f1 ?.apply sym_eq. assumption.
+  intros.simplify.intro.apply not_eq_pp_cons m x f1.apply sym_eq. assumption.
+  intros.simplify.intro.apply not_eq_nn_cons m x f1.apply sym_eq. assumption.

   intros.
    change in match (eqfb (cons x f1) (cons y g1)) 
    with (andb (eqZb x y) (eqfb f1 g1)).
   intros.
    change in match (eqfb (cons x f1) (cons y g1)) 
    with (andb (eqZb x y) (eqfb f1 g1)).


@@ -317,4 +317,4 @@ theorem rtimes_rinv: \forall r:ratio. rtimes r (rinv r) = one.
 intro.elim r.
 reflexivity.
 simplify.apply ftimes_finv.
 intro.elim r.
 reflexivity.
 simplify.apply ftimes_finv.

-qed.
\ No newline at end of file
+qed.

diff --git a/helm/matita/library/Z/plus.ma b/helm/matita/library/Z/plus.ma
index dc743e60bc77f384ecdadd927cee18d5ae085461..b89f291fbb918684cb595dbd54b5d423259e7e23 100644 (file)
--- a/helm/matita/library/Z/plus.ma
+++ b/helm/matita/library/Z/plus.ma
@@ -59,12 +59,12 @@ simplify.
 rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
 simplify.
 rewrite > nat_compare_n_m_m_n.
 rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
 simplify.
 rewrite > nat_compare_n_m_m_n.

-simplify.elim nat_compare ? ?.simplify.reflexivity.
+simplify.elim nat_compare.simplify.reflexivity.

 simplify. reflexivity.
 simplify. reflexivity.
 elim y.simplify.reflexivity.
 simplify.rewrite > nat_compare_n_m_m_n.
 simplify. reflexivity.
 simplify. reflexivity.
 elim y.simplify.reflexivity.
 simplify.rewrite > nat_compare_n_m_m_n.

-simplify.elim nat_compare ? ?.simplify.reflexivity.
+simplify.elim nat_compare.simplify.reflexivity.

 simplify. reflexivity.
 simplify. reflexivity.
 simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
 simplify. reflexivity.
 simplify. reflexivity.
 simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index c4e965fbf356f7e198a8e24f7d26d3767ad70700..a36bd078c01877187072ee6fb804fd44beaacdaa 100644 (file)
--- 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))))))).
       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))))))).
          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))))))).
          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))))))).
          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.
         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))))))).
       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))))))).
          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))))))).
          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))))))).
          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.
 
          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.
        (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 *)
 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))).
 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.
 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
 
 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.

diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma
index 443c6657f9085642d307a9f1b123a22546e11074..22c8b25a790d1551df8d23d55847352e9eb9f9b6 100644 (file)
--- a/helm/matita/library/nat/compare.ma
+++ b/helm/matita/library/nat/compare.ma
@@ -43,7 +43,7 @@ simplify.reflexivity.
 simplify.apply not_eq_O_S.
 intro.
 simplify.
 simplify.apply not_eq_O_S.
 intro.
 simplify.

-intro. apply not_eq_O_S n1 ?.apply sym_eq.assumption.
+intro. apply not_eq_O_S n1.apply sym_eq.assumption.

 intros.simplify.
 generalize in match H.
 elim (eqb n1 m1).
 intros.simplify.
 generalize in match H.
 elim (eqb n1 m1).

diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma
index ede15596aad479399b646b5f3e78ad9b423cc2fb..ad74a324db86b807cce2bbccc166c8a719fa83d2 100644 (file)
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -126,7 +126,7 @@ cut b \leq (q1-q)*b+r1.
 cut b \leq r.
 apply lt_to_not_le r b H2 Hcut2.
 elim Hcut.assumption.
 cut b \leq r.
 apply lt_to_not_le r b H2 Hcut2.
 elim Hcut.assumption.

-apply trans_le ? ((q1-q)*b) ?.
+apply trans_le ? ((q1-q)*b).

 apply le_times_n.
 apply le_SO_minus.exact H6.
 rewrite < sym_plus.
 apply le_times_n.
 apply le_SO_minus.exact H6.
 rewrite < sym_plus.


@@ -134,7 +134,7 @@ apply le_plus_n.
 rewrite < sym_times.
 rewrite > distr_times_minus.
 (* ATTENZIONE ALL' ORDINAMENTO DEI GOALS *)
 rewrite < sym_times.
 rewrite > distr_times_minus.
 (* ATTENZIONE ALL' ORDINAMENTO DEI GOALS *)

-rewrite > plus_minus ? ? ? ?.
+rewrite > plus_minus.

 rewrite > sym_times.
 rewrite < H5.
 rewrite < sym_times.
 rewrite > sym_times.
 rewrite < H5.
 rewrite < sym_times.


@@ -154,14 +154,14 @@ cut b \leq (q-q1)*b+r.
 cut b \leq r1.
 apply lt_to_not_le r1 b H4 Hcut2.
 elim Hcut.assumption.
 cut b \leq r1.
 apply lt_to_not_le r1 b H4 Hcut2.
 elim Hcut.assumption.

-apply trans_le ? ((q-q1)*b) ?.
+apply trans_le ? ((q-q1)*b).

 apply le_times_n.
 apply le_SO_minus.exact H6.
 rewrite < sym_plus.
 apply le_plus_n.
 rewrite < sym_times.
 rewrite > distr_times_minus.
 apply le_times_n.
 apply le_SO_minus.exact H6.
 rewrite < sym_plus.
 apply le_plus_n.
 rewrite < sym_times.
 rewrite > distr_times_minus.

-rewrite > plus_minus ? ? ? ?.
+rewrite > plus_minus.

 rewrite > sym_times.
 rewrite < H3.
 rewrite < sym_times.
 rewrite > sym_times.
 rewrite < H3.
 rewrite < sym_times.


@@ -275,4 +275,4 @@ apply inj_times_l m.assumption.
 qed.
 
 variant inj_times_l1:\forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q
 qed.
 
 variant inj_times_l1:\forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q

-\def lt_O_to_injective_times_l.
\ No newline at end of file
+\def lt_O_to_injective_times_l.

diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma
index a3a71522804d7eee69c2f5461d3fd7fe79d73fbf..4628eca13c1d86f1f545f95784b118f814b4832b 100644 (file)
--- a/helm/matita/library/nat/factorization.ma
+++ b/helm/matita/library/nat/factorization.ma
@@ -216,7 +216,7 @@ elim Hcut2.absurd O=r.
 apply le_n_O_to_eq.apply le_S_S_to_le.exact H5.
 simplify.intro.
 cut O=n1.
 apply le_n_O_to_eq.apply le_S_S_to_le.exact H5.
 simplify.intro.
 cut O=n1.

-apply not_le_Sn_O O ?.
+apply not_le_Sn_O O.

 rewrite > Hcut3 in \vdash (? ? %).
 assumption.rewrite > Hcut. 
 rewrite < H6.reflexivity.
 rewrite > Hcut3 in \vdash (? ? %).
 assumption.rewrite > Hcut. 
 rewrite < H6.reflexivity.


@@ -273,7 +273,7 @@ cut (S(S m1)) = r.
 rewrite > Hcut3 in \vdash (? (? ? %)).
 change with divides (nth_prime p) r \to False.
 intro.
 rewrite > Hcut3 in \vdash (? (? ? %)).
 change with divides (nth_prime p) r \to False.
 intro.

-apply plog_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r ? ? ? ?.
+apply plog_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r.

 apply lt_SO_nth_prime_n.
 simplify.apply le_S_S.apply le_O_n.apply le_n.
 assumption.
 apply lt_SO_nth_prime_n.
 simplify.apply le_S_S.apply le_O_n.apply le_n.
 assumption.


@@ -301,7 +301,7 @@ cut r \lt (S O) \or r=(S O).
 elim Hcut3.absurd O=r.
 apply le_n_O_to_eq.apply le_S_S_to_le.exact H2.
 simplify.intro.
 elim Hcut3.absurd O=r.
 apply le_n_O_to_eq.apply le_S_S_to_le.exact H2.
 simplify.intro.

-apply not_le_Sn_O O ?.
+apply not_le_Sn_O O.

 rewrite > H3 in \vdash (? ? %).assumption.assumption.
 apply le_to_or_lt_eq r (S O).
 apply not_lt_to_le.assumption.
 rewrite > H3 in \vdash (? ? %).assumption.assumption.
 apply le_to_or_lt_eq r (S O).
 apply not_lt_to_le.assumption.


@@ -400,7 +400,7 @@ intro.
 cut i = j.
 apply not_le_Sn_n i.rewrite > Hcut1 in \vdash (? ? %).assumption.
 apply injective_nth_prime ? ? H4.
 cut i = j.
 apply not_le_Sn_n i.rewrite > Hcut1 in \vdash (? ? %).assumption.
 apply injective_nth_prime ? ? H4.

-apply H i (S j) ?.
+apply H i (S j).

 apply trans_lt ? j.assumption.simplify.apply le_n.
 assumption.
 apply divides_times_to_divides.
 apply trans_lt ? j.assumption.simplify.apply le_n.
 assumption.
 apply divides_times_to_divides.


@@ -470,7 +470,7 @@ simplify in H4.
 rewrite > plus_n_O.
 rewrite > plus_n_O (defactorize_aux n3 (S i)).assumption.
 apply False_ind.
 rewrite > plus_n_O.
 rewrite > plus_n_O (defactorize_aux n3 (S i)).assumption.
 apply False_ind.

-apply not_divides_defactorize_aux n1 i (S i) ?.
+apply not_divides_defactorize_aux n1 i (S i).

 simplify. apply le_n.
 simplify in H5.
 rewrite > plus_n_O (defactorize_aux n1 (S i)).
 simplify. apply le_n.
 simplify in H5.
 rewrite > plus_n_O (defactorize_aux n1 (S i)).


@@ -480,7 +480,7 @@ apply witness ? ? ((exp (nth_prime i) n5)*(defactorize_aux n3 (S i))).
 reflexivity.
 intros.
 apply False_ind.
 reflexivity.
 intros.
 apply False_ind.

-apply not_divides_defactorize_aux n3 i (S i) ?.
+apply not_divides_defactorize_aux n3 i (S i).

 simplify. apply le_n.
 simplify in H4.
 rewrite > plus_n_O (defactorize_aux n3 (S i)).
 simplify. apply le_n.
 simplify in H4.
 rewrite > plus_n_O (defactorize_aux n3 (S i)).

diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma
index 301c0be8ef1dc689646af66e4321177c2cb5372f..3babb5c75151fe36f0cf098e055d39294164eb22 100644 (file)
--- a/helm/matita/library/nat/log.ma
+++ b/helm/matita/library/nat/log.ma
@@ -178,7 +178,7 @@ rewrite > H4.
 (* META NOT FOUND !!!  
 rewrite > sym_eq. *)
 simplify.intro.
 (* META NOT FOUND !!!  
 rewrite > sym_eq. *)
 simplify.intro.

-apply not_eq_O_S m1 ?.
+apply not_eq_O_S m1.

 rewrite > H5.reflexivity.
 qed.
 
 rewrite > H5.reflexivity.
 qed.
 

diff --git a/helm/matita/library/nat/minimization.ma b/helm/matita/library/nat/minimization.ma
index 748399fbcc699f20c308228bc8e600e64fc2a4d5..4dfda0ba69f014bdb7030dfd7d8782d46ab30817 100644 (file)
--- a/helm/matita/library/nat/minimization.ma
+++ b/helm/matita/library/nat/minimization.ma
@@ -86,7 +86,7 @@ simplify.
 apply bool_ind (\lambda b:bool.
 (f (S n1) = b) \to (f ([\lambda b:bool.nat] match b in bool with
 [ true \Rightarrow (S n1)
 apply bool_ind (\lambda b:bool.
 (f (S n1) = b) \to (f ([\lambda b:bool.nat] match b in bool with
 [ true \Rightarrow (S n1)

-| false  \Rightarrow (max n1 f)])) = true) ? ? ?.
+| false  \Rightarrow (max n1 f)])) = true).

 simplify.intro.assumption.
 simplify.intro.apply H.
 elim H1.elim H3.generalize in match H5.
 simplify.intro.assumption.
 simplify.intro.apply H.
 elim H1.elim H3.generalize in match H5.


@@ -94,7 +94,7 @@ apply le_n_Sm_elim a n1 H4.
 intros.
 apply ex_intro nat ? a.
 split.apply le_S_S_to_le.assumption.assumption.
 intros.
 apply ex_intro nat ? a.
 split.apply le_S_S_to_le.assumption.assumption.

-intros.apply False_ind.apply not_eq_true_false ?.
+intros.apply False_ind.apply not_eq_true_false.

 rewrite < H2.rewrite < H7.rewrite > H6. reflexivity.
 reflexivity.
 qed.
 rewrite < H2.rewrite < H7.rewrite > H6. reflexivity.
 reflexivity.
 qed.


@@ -163,7 +163,7 @@ simplify.
 apply bool_ind (\lambda b:bool.
 (f (m-(S n)) = b) \to (f ([\lambda b:bool.nat] match b in bool with
 [ true \Rightarrow m-(S n)
 apply bool_ind (\lambda b:bool.
 (f (m-(S n)) = b) \to (f ([\lambda b:bool.nat] match b in bool with
 [ true \Rightarrow m-(S n)

-| false  \Rightarrow (min_aux n m f)])) = true) ? ? ?.
+| false  \Rightarrow (min_aux n m f)])) = true).

 simplify.intro.assumption.
 simplify.intro.apply H.
 elim H1.elim H3.elim H4.
 simplify.intro.assumption.
 simplify.intro.apply H.
 elim H1.elim H3.elim H4.


@@ -204,7 +204,7 @@ rewrite > min_aux_O_f f n.apply le_n.
 elim min_aux_S f n1 n.
 elim H1.rewrite > H3.apply le_n.
 elim H1.rewrite > H3.
 elim min_aux_S f n1 n.
 elim H1.rewrite > H3.apply le_n.
 elim H1.rewrite > H3.

-apply trans_le (n-(S n1)) (n-n1) ?.
+apply trans_le (n-(S n1)) (n-n1).

 apply monotonic_le_minus_r.
 apply le_n_Sn.
 assumption.
 apply monotonic_le_minus_r.
 apply le_n_Sn.
 assumption.

diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 3acce20afe21277adfab0b15c6d023022afd5da5..079e902ad39ba9213b28b7b58062ed9e9db39dcb 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -82,7 +82,7 @@ qed.
 
 theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to 
 n = m+p.
 
 theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to 
 n = m+p.

-intros.apply trans_eq ? ? ((n-m)+m) ?.
+intros.apply trans_eq ? ? ((n-m)+m).

 apply plus_minus_m_m.
 apply H.elim H1.
 apply sym_plus.
 apply plus_minus_m_m.
 apply H.elim H1.
 apply sym_plus.


@@ -220,7 +220,7 @@ apply (leb_elim z y).
     apply inj_plus_l (x*z).assumption.
     apply trans_eq nat ? (x*y).
       rewrite < distr_times_plus.rewrite < plus_minus_m_m ? ? H.reflexivity.
     apply inj_plus_l (x*z).assumption.
     apply trans_eq nat ? (x*y).
       rewrite < distr_times_plus.rewrite < plus_minus_m_m ? ? H.reflexivity.

-      rewrite < plus_minus_m_m ? ? ?.
+      rewrite < plus_minus_m_m.

         reflexivity.
         apply le_times_r.assumption.
   intro.rewrite > eq_minus_n_m_O.
         reflexivity.
         apply le_times_r.assumption.
   intro.rewrite > eq_minus_n_m_O.

diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index 100cb0f0356afccc78a3b06f8c2c7e62da4953a0..aae6434e7e55657890c883550dc380d2db86275f 100644 (file)
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -97,7 +97,7 @@ intro.elim n1.
 left.reflexivity.
 right.apply not_eq_O_S.
 intro.right.intro.
 left.reflexivity.
 right.apply not_eq_O_S.
 intro.right.intro.

-apply not_eq_O_S n1 ?.
+apply not_eq_O_S n1.

 apply sym_eq.assumption.
 intros.elim H.
 left.apply eq_f. assumption.
 apply sym_eq.assumption.
 intros.elim H.
 left.apply eq_f. assumption.

diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 37c60b4057713ac77ddf68e638b2279db7f235a9..0b8f2bbe207f38580c466e45152f7cffc88cbbb2 100644 (file)
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -43,7 +43,7 @@ n < smallest_factor (S (fact n)).
 intros.
 apply not_le_to_lt.
 change with smallest_factor (S (fact n)) \le n \to False.intro.
 intros.
 apply not_le_to_lt.
 change with smallest_factor (S (fact n)) \le n \to False.intro.

-apply not_divides_S_fact n (smallest_factor(S (fact n))) ? ?.
+apply not_divides_S_fact n (smallest_factor(S (fact n))).

 apply lt_SO_smallest_factor.
 simplify.apply le_S_S.apply le_SO_fact.
 assumption.
 apply lt_SO_smallest_factor.
 simplify.apply le_S_S.apply le_SO_fact.
 assumption.