X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fnlibrary%2Fproperties%2Frelations.ma;h=334c67842f8762ecee087a7dd103f8ba0e886345;hb=df0dc72bccac82b3dd69108b5996d7008d007601;hp=1df2e205a5d097a2680ad0864d92145ada7c9906;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/matita/nlibrary/properties/relations.ma b/matitaB/matita/nlibrary/properties/relations.ma
index 1df2e205a..334c67842 100644
--- a/matitaB/matita/nlibrary/properties/relations.ma
+++ b/matitaB/matita/nlibrary/properties/relations.ma
@@ -20,7 +20,7 @@ definition transitive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀z,x,y. P x z
 
 record equivalence_relation (A:Type[0]) : Type[1] ≝
  { eq_rel:2> A → A → CProp[0];
-   refl: reflexive ? eq_rel;
-   sym: symmetric ? eq_rel;
-   trans: transitive ? eq_rel
+   refl: <A href="cic:/matita/ng/properties/relations/reflexive.def(1)">reflexive</A> ? eq_rel;
+   sym: <A href="cic:/matita/ng/properties/relations/symmetric.def(1)">symmetric</A> ? eq_rel;
+   trans: <A href="cic:/matita/ng/properties/relations/transitive.def(1)">transitive</A> ? eq_rel
  }.