diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-22 17:12:57 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-22 17:12:57 +0000 |
| commit | 3a91cd07b9399ed66b3b554b0aa173a541b4a87a (patch) | |
| tree | 19e206b870c7f09ac98a3a98dc9911d849afa7f0 /theories/Arith/Div2.v | |
| parent | 8db4a882c70008d0eefbbb90b401612906cc9629 (diff) | |
Changement nommage des hypothèses; parenthèses pour les tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@462 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Div2.v')
| -rw-r--r-- | theories/Arith/Div2.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 2040c00c4..5520e179d 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -60,8 +60,8 @@ Intro H. Absurd (div2 (S O))=(div2 (S (S O))). Simpl. Discriminate. Assumption. Split; Auto with arith. (* n = (S (S n')) *) -Intros. Decompose [and] H. Unfold iff in H1 H2. -Decompose [and] H1. Decompose [and] H2. Clear H H1 H2. +Intros. Decompose [and] H. Unfold iff in H0 H1. +Decompose [and] H0. Decompose [and] H1. Clear H H0 H1. Split; Split; Auto with arith. Intro H. Inversion H. Inversion H1. Change (S (div2 n0))=(S (div2 (S n0))). Auto with arith. @@ -109,8 +109,8 @@ Intro H. Inversion H. Split; Split; Auto with arith. Intro H. Inversion H. Inversion H1. (* n = (S (S n')) *) -Intros. Decompose [and] H. Unfold iff in H1 H2. -Decompose [and] H1. Decompose [and] H2. Clear H H1 H2. +Intros. Decompose [and] H. Unfold iff in H0 H1. +Decompose [and] H0. Decompose [and] H1. Clear H H0 H1. Split; Split. Intro H. Inversion H. Inversion H1. Simpl. Rewrite (double_S (div2 n0)). Auto with arith. |