]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cd42512) | patch
Added a demo for Matita: two slightly different proofs in declarative language
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Nov 2006 21:48:29 +0000 (21:48 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Nov 2006 21:48:29 +0000 (21:48 +0000)
commit5e97abb9c4c602db2d12963d3c6bec1517461c2c
treeb6eb3559000e7d8557816e0f366b68d0910c9604tree | snapshot
parentcd425125163b22a968f2ff1da6f80b83c35614b5commit | diff
Added a demo for Matita: two slightly different proofs in declarative language
that the derivative of x^n is n*x^(n-1). The real numbers, the definition of
derivative and some basic properties of derivatives are axiomatized. Two
alternative notations are proposed for the derivatives. (The somehow nicer
one is currently bugged.)
helm/software/matita/library/demo/power_derivative.ma [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.