]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3a3517f) | patch
- xoa: more existential types
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 18 Jun 2011 14:29:50 +0000 (14:29 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 18 Jun 2011 14:29:50 +0000 (14:29 +0000)
commit331cbed42a29b3b9f5fb11d127534f3c62c86797
treebfc350ffb8552468348ea093aaaef658897e3d47tree | snapshot
parent3a3517f9a23d9344ff6461e76e1c6c429d44db57commit | diff
- xoa: more existential types
- ground: more arithmetics
- lift: more nasic inversion lemmas and some renaming
matita/matita/lib/lambda-delta/ground.ma diff | blob | history
matita/matita/lib/lambda-delta/substitution/lift_defs.ma diff | blob | history
matita/matita/lib/lambda-delta/substitution/lift_main.ma diff | blob | history
matita/matita/lib/lambda-delta/xoa_defs.ma diff | blob | history
matita/matita/lib/lambda-delta/xoa_notation.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.