Keeping track of locations of disambiguated ids and symbols.

[helm.git] / matitaB / matita / nlibrary / properties / relations2.ma

diff --git a/matitaB/matita/nlibrary/properties/relations2.ma b/matitaB/matita/nlibrary/properties/relations2.ma
index 67d09e9383c91f00c081479404456ea19096da25..155dde75b274e488ef24cf31bc02844f852610bc 100644 (file)
--- a/matitaB/matita/nlibrary/properties/relations2.ma
+++ b/matitaB/matita/nlibrary/properties/relations2.ma
@@ -14,13 +14,13 @@
 
 include "logic/pts.ma".
 
-ndefinition reflexive2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀x.P x x.
-ndefinition symmetric2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀x,y.P x y → P y x.
-ndefinition transitive2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀z,x,y. P x z → P z y → P x y.
+definition reflexive2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀x.P x x.
+definition symmetric2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀x,y.P x y → P y x.
+definition transitive2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀z,x,y. P x z → P z y → P x y.
 
-nrecord equivalence_relation2 (A:Type[2]) : Type[3] ≝
+record equivalence_relation2 (A:Type[2]) : Type[3] ≝
  { eq_rel2:2> A → A → CProp[2];
-   refl2: reflexive2 ? eq_rel2;
-   sym2: symmetric2 ? eq_rel2;
-   trans2: transitive2 ? eq_rel2
+   refl2: <A href="cic:/matita/ng/properties/relations2/reflexive2.def(1)">reflexive2</A> ? eq_rel2;
+   sym2: <A href="cic:/matita/ng/properties/relations2/symmetric2.def(1)">symmetric2</A> ? eq_rel2;
+   trans2: <A href="cic:/matita/ng/properties/relations2/transitive2.def(1)">transitive2</A> ? eq_rel2
  }.