]> matita.cs.unibo.it Git - helm.git/commit
update in basic_2
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 4 Mar 2018 18:59:20 +0000 (19:59 +0100)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 4 Mar 2018 18:59:20 +0000 (19:59 +0100)
commit47a745462a714af9d65cea7b61af56524bd98fa1
tree8967c46fcf645f8975522e86ec83796e1d4cbb84
parent990f97071a9939d47be16b36f6045d3b23f218e0
update in basic_2

+ new proof of cpx_frees_conf_lexs with fsle
+ refactoring
43 files changed:
matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma
matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lex_length.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_ext.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc2.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fsle.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lfxs.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_etc.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfeq.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_cpx.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_etc.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fsle.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_length.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma
matita/matita/contribs/lambdadelta/basic_2/static/fle.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
matita/matita/contribs/lambdadelta/basic_2/static/frees_append.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/fsle_drops.ma
matita/matita/contribs/lambdadelta/basic_2/static/fsle_length.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fsle.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma
matita/matita/contribs/lambdadelta/basic_2/syntax/append.ma
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl