X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fnlibrary%2Fproperties%2Frelations1.ma;h=535a11984524b5978c6fc4092129b3befaada052;hb=6d4277977478ef9bcadaffbef3d4bb04ac0250a5;hp=86a6f15b707b61318ab122c766db38c6fef4bc85;hpb=98f0fac6d03367be776303e7ba353b75878aaa40;p=helm.git

diff --git a/matitaB/matita/nlibrary/properties/relations1.ma b/matitaB/matita/nlibrary/properties/relations1.ma
index 86a6f15b7..535a11984 100644
--- a/matitaB/matita/nlibrary/properties/relations1.ma
+++ b/matitaB/matita/nlibrary/properties/relations1.ma
@@ -14,13 +14,13 @@
 
 include "logic/pts.ma".
 
-ndefinition reflexive1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀x.P x x.
-ndefinition symmetric1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀x,y.P x y → P y x.
-ndefinition transitive1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀z,x,y. P x z → P z y → P x y.
+definition reflexive1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀x.P x x.
+definition symmetric1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀x,y.P x y → P y x.
+definition transitive1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀z,x,y. P x z → P z y → P x y.
 
-nrecord equivalence_relation1 (A:Type[1]) : Type[2] ≝
+record equivalence_relation1 (A:Type[1]) : Type[2] ≝
  { eq_rel1:2> A → A → CProp[1];
-   refl1: reflexive1 ? eq_rel1;
-   sym1: symmetric1 ? eq_rel1;
-   trans1: transitive1 ? eq_rel1
+   refl1: <A href="cic:/matita/ng/properties/relations1/reflexive1.def(1)">reflexive1</A> ? eq_rel1;
+   sym1: <A href="cic:/matita/ng/properties/relations1/symmetric1.def(1)">symmetric1</A> ? eq_rel1;
+   trans1: <A href="cic:/matita/ng/properties/relations1/transitive1.def(1)">transitive1</A> ? eq_rel1
  }.