ocaml 3.09 transition

[helm.git] / helm / matita / library / Z / compare.ma

diff --git a/helm/matita/library/Z/compare.ma b/helm/matita/library/Z/compare.ma
index 3b259b4f664b0b19d1d8ec646596600e135e693e..4a5025975fe3d8d4b3f610563b565dce39be6bac 100644 (file)
--- a/helm/matita/library/Z/compare.ma
+++ b/helm/matita/library/Z/compare.ma
@@ -41,7 +41,7 @@ theorem eqZb_to_Prop:
 \forall x,y:Z. 
 match eqZb x y with
 [ true \Rightarrow x=y
-| false \Rightarrow \lnot x=y].
+| false \Rightarrow x \neq y].
 intros.
 elim x.
   elim y.
@@ -49,31 +49,31 @@ 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.
-(x=y \to (P true)) \to (\lnot x=y \to (P false)) \to P (eqZb x y).
+(x=y \to (P true)) \to (x \neq y \to (P false)) \to P (eqZb x y).
 intros.
 cut 
-match (eqZb x y) with
+(match (eqZb x y) with
 [ true \Rightarrow x=y
-| false \Rightarrow \lnot x=y] \to P (eqZb x y).
+| false \Rightarrow x \neq y] \to P (eqZb x y)).
 apply Hcut.
 apply eqZb_to_Prop.
 elim (eqZb).
-apply H H2.
-apply H1 H2.
+apply (H H2).
+apply (H1 H2).
 qed.
 
 definition Z_compare : Z \to Z \to compare \def
@@ -109,14 +109,14 @@ elim x.
   elim y.
     simplify.exact I.
     simplify.
-      cut match (nat_compare n n1) with
+      cut (match (nat_compare n n1) with
       [ LT \Rightarrow n<n1
       | EQ \Rightarrow n=n1
       | GT \Rightarrow n1<n] \to 
       match (nat_compare n n1) with
       [ LT \Rightarrow (S n) \leq n1
       | EQ \Rightarrow pos n = pos n1
-      | GT \Rightarrow (S n1) \leq n]. 
+      | GT \Rightarrow (S n1) \leq n]). 
         apply Hcut.apply nat_compare_to_Prop. 
         elim (nat_compare n n1).
           simplify.exact H.
@@ -127,14 +127,14 @@ elim x.
     simplify.exact I.
     simplify.exact I.
     simplify. 
-      cut match (nat_compare n1 n) with
+      cut (match (nat_compare n1 n) with
       [ LT \Rightarrow n1<n
       | EQ \Rightarrow n1=n
       | GT \Rightarrow n<n1] \to 
       match (nat_compare n1 n) with
       [ LT \Rightarrow (S n1) \leq n
       | EQ \Rightarrow neg n = neg n1
-      | GT \Rightarrow (S n) \leq n1]. 
+      | GT \Rightarrow (S n) \leq n1]). 
         apply Hcut. apply nat_compare_to_Prop. 
         elim (nat_compare n1 n).
           simplify.exact H.