() around tactic terms

[helm.git] / helm / matita / library / nat / minus.ma

diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 1ee70bd39c0a19088ebc2fb1d12dfbdf28add444..00a90acd83192ee2d79d6b8b59c7a1e37d2e21ff 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -227,9 +227,9 @@ qed.
 
 (* minus and lt - to be completed *)
 theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p).
-intros 3.apply nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p)).
+intros 3.apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p))).
 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
-simplify.intros.apply False_ind.apply not_le_Sn_O n H.
+simplify.intros.apply False_ind.apply (not_le_Sn_O n H).
 simplify.intros.
 apply le_S_S.
 rewrite < plus_n_Sm.