ocaml 3.09 transition

[helm.git] / helm / matita / library / nat / nth_prime.ma

diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 5fa636301425eb1354b40403b374c54e860134f1..5330f52adbb923ddd84fc91ac1a876b373751ccc 100644 (file)
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -45,10 +45,10 @@ apply not_le_to_lt.
 change with (smallest_factor (S n!) \le n \to False).intro.
 apply (not_divides_S_fact n (smallest_factor(S n!))).
 apply lt_SO_smallest_factor.
-simplify.apply le_S_S.apply le_SO_fact.
+unfold lt.apply le_S_S.apply le_SO_fact.
 assumption.
 apply divides_smallest_factor_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
 theorem ex_prime: \forall n. (S O) \le n \to \exists m.
@@ -66,7 +66,7 @@ apply le_smallest_factor_n.
 apply prime_smallest_factor_n.
 change with ((S(S O)) \le S (S n1)!).
 apply le_S.apply le_SSO_fact.
-simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
 qed.
 
 let rec nth_prime n \def
@@ -147,14 +147,14 @@ apply increasing_nth_prime.
 qed.
 
 theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
-intros. elim n.simplify.apply le_n.
+intros. elim n.unfold lt.apply le_n.
 apply (trans_lt ? (nth_prime n1)).
 assumption.apply lt_nth_prime_n_nth_prime_Sn.
 qed.
 
 theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
 intros.apply (trans_lt O (S O)).
-simplify. apply le_n.apply lt_SO_nth_prime_n.
+unfold lt. apply le_n.apply lt_SO_nth_prime_n.
 qed.
 
 theorem ex_m_le_n_nth_prime_m: 
@@ -195,6 +195,6 @@ apply (lt_nth_prime_to_not_prime a).assumption.assumption.
 apply (ex_intro nat ? a).assumption.
 apply le_to_or_lt_eq.assumption.
 apply ex_m_le_n_nth_prime_m.
-simplify.simplify in H.elim H.assumption.
+simplify.unfold prime in H.elim H.assumption.
 qed.