]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b15a4df) | patch
Some refactoring in set*.ma, some new notations and new hints for \cup.
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 9 Sep 2010 22:14:11 +0000 (22:14 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 9 Sep 2010 22:14:11 +0000 (22:14 +0000)
commitfd6a295e279aa5cc6b8eda610e25f3fbdb2f8d43
treeb7e6d68ec01ee4a9074758818fa26d229748546etree | snapshot
parentb15a4df27469ee4b64d1b3b8fc996cd15e8a61f0commit | diff
Some refactoring in set*.ma, some new notations and new hints for \cup.
non uniform coercions still to be pushed from re-setoids.ma to a place
before sets.ma, maybe in hints_declaration.ma since they are complementary.
helm/software/matita/nlibrary/re/re-setoids.ma diff | blob | history
helm/software/matita/nlibrary/sets/setoids.ma diff | blob | history
helm/software/matita/nlibrary/sets/setoids1.ma diff | blob | history
helm/software/matita/nlibrary/sets/sets.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.