]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ce747c4) | patch
- strong normalization of abbreviation proved
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 11 Feb 2012 19:48:08 +0000 (19:48 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 11 Feb 2012 19:48:08 +0000 (19:48 +0000)
commit265099f14790d32ae6b51dd72f6256d7fcb6b814
tree967db74ab61a10f32aa4da278abb02f10cddb054tree | snapshot
parentce747c4d4c3a087e1f59dca81b7b4962ffa8e02bcommit | diff
- strong normalization of abbreviation proved
- bug fix in the generation lemma for abbreviationof context=sensitive parallel reduction
matita/matita/contribs/lambda_delta/Basic_2/computation/cprs.ma diff | blob | history
matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma diff | blob | history
matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cprs.ma [new file with mode: 0644] blob
matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma [new file with mode: 0644] blob
matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma diff | blob | history
matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpss.ma diff | blob | history
matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr_cpr.ma [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.