From ac6c6c1f9934fefb4e462f3aa3e1429460703037 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 25 Oct 2006 12:51:56 +0000 Subject: [PATCH 1/1] Added timeouts to auto here and there. --- helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma b/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma index 7d8a9e3b3..661e00ecd 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 [ apply (eq_gen_succ_zero ? ? H) | lapply linear eq_gen_succ_succ to H2 as H0. subst. - apply ex_intro; [|auto new] (**) + apply ex_intro; [|auto new timeout=30] (**) ]. qed. @@ -34,7 +34,7 @@ theorem nle_gen_succ_succ: \forall x,y. x < succ y \to x <= y. [ apply (eq_gen_succ_zero ? ? H) | lapply linear eq_gen_succ_succ to H2 as H0. lapply linear eq_gen_succ_succ to H3 as H2. - subst. auto new + subst. auto new timeout=30 ]. qed. @@ -46,7 +46,7 @@ qed. theorem nle_gen_zero_2: \forall x. x <= zero \to x = zero. intros 1. elim x; clear x; intros; - [ auto new + [ auto new timeout=30 | apply (nle_gen_succ_zero ? ? H1) ]. qed. @@ -54,8 +54,8 @@ qed. theorem nle_gen_succ_2: \forall y,x. x <= succ y \to x = zero \lor \exists z. x = succ z \land z <= y. intros 2; elim x; clear x; intros; - [ auto new + [ auto new timeout=30 | lapply linear nle_gen_succ_succ to H1. - right. apply ex_intro; [|auto new] (**) + right. apply ex_intro; [|auto new timeout=30] (**) ]. qed. -- 2.39.2