- new tactic applyP for use in the *P*rocedural script reconstruction

[helm.git] / helm / software / matita / contribs / dama / dama / models / nat_lebesgue.ma

diff --git a/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma b/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma
index 7e059c03d96d2bc37c86a73ae02d5189dd272e9e..8b062b6ded457bad06717da766967b76902de547 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_lebesgue.ma
@@ -21,7 +21,7 @@ theorem nat_lebesgue_oc:
      ∀x:ℕ.a order_converges x → 
       x ∈ [l,u] ∧ 
       ∀h:x ∈ [l,u].
-       uniform_converge {[l,u]} (⌊n,〈a n,H n〉⌋) 〈x,h〉.
+       uniform_converge {[l,u]} ⌊n,〈a n,H n〉⌋ 〈x,h〉.
 intros; apply lebesgue_oc; [apply nat_us_is_oc] assumption;
 qed.