diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-14 14:01:34 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-14 14:01:34 +0000 |
| commit | a78317340764034355e144947b87ba7015a8769d (patch) | |
| tree | 69363dc6e4806f3a7c3de8de189a6d0a8dd234ec /theories/Init/Logic.v | |
| parent | e542de6a7f8e618c3f7f3997696e91774c50a3f9 (diff) | |
Automatisation de la traduction de iff_trans; renommage IF
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4903 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init/Logic.v')
| -rwxr-xr-x | theories/Init/Logic.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 4c284818b..dc067a4b7 100755 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -78,7 +78,7 @@ Theorem iff_refl : (A:Prop) (iff A A). Split; Auto. Qed. -Theorem iff_trans : (A,B,C:Prop) (iff A B) -> (iff B C) -> (iff A C). +Theorem iff_trans : (a,b,c:Prop) (iff a b) -> (iff b c) -> (iff a c). Proof. Intros A B C (H1,H2) (H3,H4); Split; Auto. Qed. @@ -92,7 +92,8 @@ End Equivalence. (** [(IF P Q R)], or more suggestively [(either P and_then Q or_else R)], denotes either [P] and [Q], or [~P] and [Q] *) -Definition IF := [P,Q,R:Prop] (or (and P Q) (and (not P) R)). +Definition IF_then_else := [P,Q,R:Prop] (or (and P Q) (and (not P) R)). +V7only [Notation IF:=IF_then_else.]. Notation "'IF' c1 'then' c2 'else' c3" := (IF c1 c2 c3) (at level 1, c1, c2, c3 at level 8) : type_scope |