From 4a8716e06131e53392eab754f859eb01fc02fdde Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 6 Jan 2007 16:14:06 +0000 Subject: [PATCH] ;auto fixed --- helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma | 2 +- helm/software/matita/contribs/RELATIONAL/NLE/props.ma | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma b/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma index 5ddeb41af..afefbfd4d 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma @@ -25,7 +25,7 @@ theorem nle_gen_succ_1: \forall x,y. x < y \to intros. decompose. lapply linear nplus_gen_succ_2 to H1 as H. decompose. subst. - apply ex_intro; auto. (**) + apply ex_intro;[| auto] (**) qed. diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma index b571dfc6b..549eae418 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma @@ -24,7 +24,7 @@ qed. theorem nle_succ: \forall p,q. p <= q \to succ p <= succ q. unfold NLE. intros. decompose. - apply ex_intro; auto. (**) + apply ex_intro; [|auto] (**) qed. theorem nle_refl: \forall x. x <= x. -- 2.39.2