Keeping track of locations of disambiguated ids and symbols.

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

diff --git a/matitaB/matita/nlibrary/properties/relations1.ma b/matitaB/matita/nlibrary/properties/relations1.ma
index 86a6f15b707b61318ab122c766db38c6fef4bc85..535a11984524b5978c6fc4092129b3befaada052 100644 (file)
--- 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
  }.