]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 85fce74) | patch
We begin to play the real game: we have defined real numbers and
authorEnrico Zoli <??>
Tue, 31 Oct 2006 18:23:36 +0000 (18:23 +0000)
committerEnrico Zoli <??>
Tue, 31 Oct 2006 18:23:36 +0000 (18:23 +0000)
commitbf45bade243d89f2171e76e8eaa9a58489eda45c
tree6a66d752d6461f2184a19868265cc7f631ad9afftree | snapshot
parent85fce74d6a0cd8e83e59895e81f1bc09d21ef4c2commit | diff
We begin to play the real game: we have defined real numbers and
constructive connectives (only the disjunction for now) and we are
trying to define the max between two real numbers as the limit of a
particular cauchy sequence. Cool.
helm/software/matita/dama/constructive_connectives.ma [new file with mode: 0644] blob
helm/software/matita/dama/groups.ma diff | blob | history
helm/software/matita/dama/integration_algebras.ma diff | blob | history
helm/software/matita/dama/ordered_fields_ch0.ma diff | blob | history
helm/software/matita/dama/reals.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.