]> matita.cs.unibo.it Git - helm.git/commit
update in ground
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 19 May 2022 10:11:11 +0000 (12:11 +0200)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 19 May 2022 10:11:11 +0000 (12:11 +0200)
commit77479649510792efe4d9cbff508e118360862594
tree472549f45687ee0556e8cbae3623b4cf8b3888d8
parent9b4e20442ec5a4028cfe2b6fe836c94acdb033b8
update in ground

+ new notation for application of a relocation
65 files changed:
matita/matita/contribs/lambdadelta/apps_2/functional/flifts.ma
matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma
matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
matita/matita/contribs/lambdadelta/delayed_updating/unwind/nap.ma
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma
matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_constructors.ma
matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_depth.ma
matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma
matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_update.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma
matita/matita/contribs/lambdadelta/ground/notation/functions/atsharp_2.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground/notation/relations/rat_3.ma [deleted file]
matita/matita/contribs/lambdadelta/ground/notation/relations/ratsharp_3.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma
matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after_ist.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat_tls.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat_uni_tls.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isf.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isi.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_pat_tls.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_pat.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_ist.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_isi.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_nat.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_pat.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_basic.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_id.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_lt.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_pat.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_pat_id.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_tls.ma
matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_uni.ma
matita/matita/contribs/lambdadelta/ground/relocation/tr_compose.ma
matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pap.ma
matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma
matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.ma
matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_eq.ma
matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pap.ma
matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pat.ma
matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma
matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pushs.ma
matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
matita/matita/contribs/lambdadelta/ground/relocation/tr_pat.ma
matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_pap.ma
matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
matita/matita/contribs/lambdadelta/static_2/relocation/drops.ma
matita/matita/predefined_virtuals.ml