diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-11 12:41:41 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-11 12:41:41 +0000 |
| commit | 4ac0580306ea9e45da1863316936d700969465ad (patch) | |
| tree | bf7595cd76895f3a349e7e75ca9d64231b01dcf8 /theories/Wellfounded | |
| parent | 8a7452976731275212f0c464385b380e2d590f5e (diff) | |
documentation automatique de la bibliothèque standard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1578 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Wellfounded')
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Product.v | 4 | ||||
| -rwxr-xr-x | theories/Wellfounded/intro.tex | 4 |
2 files changed, 6 insertions, 2 deletions
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index a51b876ab..419f545f5 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -91,7 +91,7 @@ Section Wf_Symmetric_Product. Syntactic Definition Symprod := (symprod A B leA leB). -(* +(*i Local sig_prod:= [x:A*B]<{_:A&B}>Case x of [a:A][b:B](existS A [_:A]B a b) end. @@ -108,7 +108,7 @@ Proof. (Apply right_lex;Auto with sets). Save. -*) +i*) Lemma Acc_symprod: (x:A)(Acc A leA x)->(y:B)(Acc B leB y) ->(Acc (A*B) Symprod (x,y)). diff --git a/theories/Wellfounded/intro.tex b/theories/Wellfounded/intro.tex new file mode 100755 index 000000000..126071e28 --- /dev/null +++ b/theories/Wellfounded/intro.tex @@ -0,0 +1,4 @@ +\section{Well-founded relations}\label{Wellfounded} + +This library gives definitions and results about well-founded relations. + |