index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Reals
Mode
Name
Size
-rw-r--r--
Alembert.v
29543
log
plain
-rw-r--r--
Alembert_compl.v
10474
log
plain
-rw-r--r--
AltSeries.v
18763
log
plain
-rw-r--r--
Binome.v
9670
log
plain
-rw-r--r--
Cauchy_prod.v
14004
log
plain
-rw-r--r--
Cos_plus.v
35610
log
plain
-rw-r--r--
Cos_rel.v
14705
log
plain
-rw-r--r--
Cv_prop.v
9541
log
plain
-rw-r--r--
DiscrR.v
1808
log
plain
-rw-r--r--
Exp_prop.v
30297
log
plain
-rw-r--r--
NewtonInt.v
30620
log
plain
-rw-r--r--
PSeries_reg.v
22025
log
plain
-rw-r--r--
R_Ifp.v
26956
log
plain
-rw-r--r--
R_sqr.v
10827
log
plain
-rw-r--r--
R_sqrt.v
13379
log
plain
-rw-r--r--
Ranalysis.v
642
log
plain
-rw-r--r--
Ranalysis1.v
45323
log
plain
-rw-r--r--
Ranalysis2.v
16225
log
plain
-rw-r--r--
Ranalysis3.v
27688
log
plain
-rw-r--r--
Ranalysis4.v
34457
log
plain
-rw-r--r--
Raxioms.v
5138
log
plain
-rw-r--r--
Rbase.v
44539
log
plain
-rw-r--r--
Rbasic_fun.v
16266
log
plain
-rw-r--r--
Rcomplet.v
23467
log
plain
-rw-r--r--
Rdefinitions.v
1440
log
plain
-rw-r--r--
Rderiv.v
20691
log
plain
-rw-r--r--
Reals.v
1227
log
plain
-rw-r--r--
Rfunctions.v
19258
log
plain
-rw-r--r--
Rgeom.v
6477
log
plain
-rw-r--r--
Rlimit.v
23475
log
plain
-rw-r--r--
Rpower.v
22513
log
plain
-rw-r--r--
Rprod.v
6229
log
plain
-rw-r--r--
Rseries.v
9668
log
plain
-rw-r--r--
Rsigma.v
5324
log
plain
-rw-r--r--
Rsqrt_def.v
19814
log
plain
-rw-r--r--
Rsyntax.v
8132
log
plain
-rw-r--r--
Rtopology.v
73837
log
plain
-rw-r--r--
Rtrigo.v
60882
log
plain
-rw-r--r--
Rtrigo_alt.v
28749
log
plain
-rw-r--r--
Rtrigo_calc.v
14670
log
plain
-rw-r--r--
Rtrigo_def.v
16801
log
plain
-rw-r--r--
Rtrigo_fun.v
5359
log
plain
-rw-r--r--
Rtrigo_reg.v
21446
log
plain
-rw-r--r--
SplitAbsolu.v
907
log
plain
-rw-r--r--
SplitRmult.v
759
log
plain
-rw-r--r--
Sqrt_reg.v
12022
log
plain
-rw-r--r--
TAF.v
19844
log
plain
-rw-r--r--
TypeSyntax.v
1178
log
plain
-rw-r--r--
intro.tex
122
log
plain