]> matita.cs.unibo.it Git - helm.git/commit
- lambdadelta: first commutation property on lazy equivalence for
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 1 Nov 2013 16:10:29 +0000 (16:10 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 1 Nov 2013 16:10:29 +0000 (16:10 +0000)
commit54fa4874fc4bfccd061b40d8353cd75a578e99ae
treea94557e569da1585b2374a808fb64bc3effbda2f
parent56e23ea031f695e40879053ff09e97ecec2507e1
- lambdadelta: first commutation property on lazy equivalence for
local environments proved (lleq_fqu_trans)
- matitadep: now three input syntaxes from grep are understood
13 files changed:
matita/components/binaries/matitadep/matitadep.ml
matita/matita/contribs/lambdadelta/basic_2/grammar/cl_restricted_weight.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma
matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma
matita/matita/contribs/lambdadelta/basic_2/notation/functions/weight_2.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_fqu.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_fquq.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
matita/matita/contribs/lambdadelta/ground_2/star.ma