diff options
| author |  Thomas Sibut-Pinote <thomas.sibut-pinote@inria.fr> | 2017-02-01 17:58:32 +0100 |
|---|---|---|
| committer | Thomas Sibut-Pinote <thomas.sibut-pinote@inria.fr> | 2017-02-15 17:56:14 +0100 |
| commit | f5c81ac1bcae7c40d5e89229647c06c97b5ddc85 (patch) | |
| tree | a5a2769d37103cdf9aff3314cc451b340b86ca18 /theories/Reals/Ranalysis5.v | |
| parent | c17c3faee20251cd5c7168246e9ffcd12d557f85 (diff) | |
Added some theory on powerRZ.
For this, I used a new inductive type Z_spec to reason on Z.
Diffstat (limited to 'theories/Reals/Ranalysis5.v')
0 files changed, 0 insertions, 0 deletions