]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7bc72d8) | patch
New version: only new nodes are normalized; moreover, reduction stops as soon
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 5 Mar 2009 11:47:13 +0000 (11:47 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 5 Mar 2009 11:47:13 +0000 (11:47 +0000)
commitdd70926289053cdc003776a5074d2262a2ec8243
tree918969905487e9ea0d4a5157f79f21c158bec4aftree | snapshot
parent7bc72d8afaebb1d2070a26b07f9bf4242b648e2ccommit | diff
New version: only new nodes are normalized; moreover, reduction stops as soon
as the term becomes shorter.
helm/software/matita/contribs/formal_topology/bin/Makefile diff | blob | history
helm/software/matita/contribs/formal_topology/bin/comb.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.