added do_heavy_checks documentation

[helm.git] / helm / software / matita / dama / classical_pointfree / ordered_sets2.ma

diff --git a/helm/software/matita/dama/classical_pointfree/ordered_sets2.ma b/helm/software/matita/dama/classical_pointfree/ordered_sets2.ma
index dafa0df4f5b71117e6f77c28a9b9d61c34731d50..d85a02cf4a633f03f1a05bad598de77a58e034c7 100644 (file)
--- a/helm/software/matita/dama/classical_pointfree/ordered_sets2.ma
+++ b/helm/software/matita/dama/classical_pointfree/ordered_sets2.ma
@@ -61,7 +61,7 @@ theorem le_to_le_sup_sup:
 qed. 
 
 interpretation "mk_bounded_sequence" 'hide_everything_but a
-= (cic:/matita/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _).
+= (cic:/matita/ordered_set/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _).
 
 lemma reduce_bas_seq:
  ∀O:ordered_set.∀a:nat→O.∀p.∀i.