Minor changes.

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

diff --git a/matita/library/nat/ord.ma b/matita/library/nat/ord.ma
index ba08a0dcf5ba21536cb4830f10c22e88b5eac00a..b7d02f87f3959afdcf85a584e1b2d738983ceb3f 100644 (file)
--- a/matita/library/nat/ord.ma
+++ b/matita/library/nat/ord.ma
@@ -215,7 +215,7 @@ apply (absurd ? ? H10 H5).
 apply (absurd ? ? H10 H7).
 (* rewrite > H6.
 rewrite > H8. *)
-auto paramodulation library=yes.
+auto paramodulation.
 unfold prime in H. elim H. assumption.
 qed.