]> matita.cs.unibo.it Git - helm.git/commit - matita/matita/lib/lambda-delta/xoa_defs.ma
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dde568d) | patch
tpr: more inversion lemmas and a main property stated
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 26 Jul 2011 19:47:31 +0000 (19:47 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 26 Jul 2011 19:47:31 +0000 (19:47 +0000)
commit4c4b73b9ccf2e93901d0352599623c851781b74b
tree238b5f4ef0ab5aa1127536cd6d07db55f84f05c7tree | snapshot
parentdde568d876a5d2e1b6e554a526c98b09b145d25acommit | diff
tpr: more inversion lemmas and a main property stated
matita/matita/lib/lambda-delta/reduction/tpr_defs.ma diff | blob | history
matita/matita/lib/lambda-delta/reduction/tpr_ps.ma [new file with mode: 0644] blob
matita/matita/lib/lambda-delta/reduction/tpr_tpr.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.