matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Enrico Zoli <??>
	Tue, 31 Oct 2006 18:23:36 +0000 (18:23 +0000)
committer	Enrico Zoli <??>
	Tue, 31 Oct 2006 18:23:36 +0000 (18:23 +0000)
commit	348acb421355c345a9af0754c1c16508a43eeea5
tree	735d89771ff13cceb6ff168b9e3561acde599a48	tree \| snapshot
parent	8b62b96fea74985e303e093d9b7ead91089c664e	commit \| 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.

matita/dama/constructive_connectives.ma	[new file with mode: 0644]	blob
matita/dama/groups.ma		diff \| blob \| history
matita/dama/integration_algebras.ma		diff \| blob \| history
matita/dama/ordered_fields_ch0.ma		diff \| blob \| history
matita/dama/reals.ma		diff \| blob \| history

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom