X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fnlibrary%2Fproperties%2Frelations.ma;fp=matita%2Fmatita%2Fnlibrary%2Fproperties%2Frelations.ma;h=1df2e205a5d097a2680ad0864d92145ada7c9906;hb=83d2e9c93f39464715e10fab6ebdb4be97c37b08;hp=581208d9afb8fcf567a4f931b8fe16f6899edeb2;hpb=559a4d0ba0e52c99822ac636b1d635611ed9b5b8;p=helm.git

diff --git a/matita/matita/nlibrary/properties/relations.ma b/matita/matita/nlibrary/properties/relations.ma
index 581208d9a..1df2e205a 100644
--- a/matita/matita/nlibrary/properties/relations.ma
+++ b/matita/matita/nlibrary/properties/relations.ma
@@ -14,11 +14,11 @@
 
 include "logic/pts.ma".
 
-ndefinition reflexive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x.P x x.
-ndefinition symmetric ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x,y.P x y → P y x.
-ndefinition transitive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀z,x,y. P x z → P z y → P x y.
+definition reflexive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x.P x x.
+definition symmetric ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x,y.P x y → P y x.
+definition transitive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀z,x,y. P x z → P z y → P x y.
 
-nrecord equivalence_relation (A:Type[0]) : Type[1] ≝
+record equivalence_relation (A:Type[0]) : Type[1] ≝
  { eq_rel:2> A → A → CProp[0];
    refl: reflexive ? eq_rel;
    sym: symmetric ? eq_rel;