]> matita.cs.unibo.it Git - helm.git/commit
- commit of the "substitution" component
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 17 Jan 2014 17:45:00 +0000 (17:45 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 17 Jan 2014 17:45:00 +0000 (17:45 +0000)
commite5378812c068074f0ac627541d3f066e135c8824
tree8c6b0cd3deac5a7d69deda550ad7863fb5c3db95
parent928cfe1ebf2fbd31731c8851cdec70802596016d
- commit of the "substitution" component
- some renaming
- we disabled the old notation for ldrop to capture its instances
syntactically
38 files changed:
matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma
matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrops.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma
matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl