X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FQ%2Fq.ma;h=340154979777529f94387cd1c630c6234cf21ab5;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=d69e459acde20c6523d82872d24c08fc42dc1b7d;hpb=fb94e5a71be508516514dfe50528ccfb3cd2da91;p=helm.git

diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma
index d69e459ac..340154979 100644
--- a/helm/matita/library/Q/q.ma
+++ b/helm/matita/library/Q/q.ma
@@ -92,13 +92,13 @@ definition ftl \def
     | (cons x f) \Rightarrow f].
     
 theorem injective_pp : injective nat fraction pp.
-simplify.intros.
+unfold injective.intros.
 change with ((aux (pp x)) = (aux (pp y))).
 apply eq_f.assumption.
 qed.
 
 theorem injective_nn : injective nat fraction nn.
-simplify.intros.
+unfold injective.intros.
 change with ((aux (nn x)) = (aux (nn y))).
 apply eq_f.assumption.
 qed.
@@ -118,7 +118,7 @@ apply eq_f.assumption.
 qed.
 
 theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.
-intros.simplify. intro.
+intros.unfold Not. intro.
 change with match (pp n) with
 [ (pp n) \Rightarrow False
 | (nn n) \Rightarrow True
@@ -130,7 +130,7 @@ qed.
 theorem not_eq_pp_cons: 
 \forall n:nat.\forall x:Z. \forall f:fraction. 
 pp n \neq cons x f.
-intros.simplify. intro.
+intros.unfold Not. intro.
 change with match (pp n) with
 [ (pp n) \Rightarrow False
 | (nn n) \Rightarrow True
@@ -142,7 +142,7 @@ qed.
 theorem not_eq_nn_cons: 
 \forall n:nat.\forall x:Z. \forall f:fraction. 
 nn n \neq cons x f.
-intros.simplify. intro.
+intros.unfold Not. intro.
 change with match (nn n) with
 [ (pp n) \Rightarrow True
 | (nn n) \Rightarrow False
@@ -153,7 +153,7 @@ qed.
 
 theorem decidable_eq_fraction: \forall f,g:fraction.
 decidable (f = g).
-intros.simplify.
+intros.unfold decidable.
 apply (fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False))).
   intros.elim g1.
     elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
@@ -188,16 +188,16 @@ intros.apply (fraction_elim2
   intros.elim g1.
     simplify.apply eqb_elim.
       intro.simplify.apply eq_f.assumption.
-      intro.simplify.intro.apply H.apply injective_pp.assumption.
+      intro.simplify.unfold Not.intro.apply H.apply injective_pp.assumption.
     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.unfold Not.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.
+    intro.simplify.unfold Not.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.unfold Not.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption.
+  intros.simplify.unfold Not.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)).
@@ -205,8 +205,8 @@ intros.apply (fraction_elim2
       intro.generalize in match H.elim (eqfb f1 g1).
         simplify.apply eq_f2.assumption.
         apply H2.
-      simplify.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption.
-      intro.simplify.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption.
+      simplify.unfold Not.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption.
+      intro.simplify.unfold Not.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption.
 qed.
 
 let rec finv f \def
@@ -243,7 +243,7 @@ let rec ftimes f g \def
         | (frac h) \Rightarrow frac (cons (x + y) h)]]].
         
 theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
-simplify. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)).
+unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)).
   intros.elim g.
     change with (Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n)).
      apply eq_f.apply sym_Zplus.