]> matita.cs.unibo.it Git - helm.git/commit
- lambdadelta: first recursive part of preservation finally proved!
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 28 Feb 2013 18:14:27 +0000 (18:14 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 28 Feb 2013 18:14:27 +0000 (18:14 +0000)
commit514f515ecb8765c68720e880460c2457898d74dc
treeb91e4a87eb4bf32bd60b76668b550c3e3660cb95
parent7bcf8e0196e9bae753396be2ba56a7ba9b808fd5
- lambdadelta: first recursive part of preservation finally proved!
- lambda: bugfix in include paths, now they are relative to the root
- matita.lang: keyword "fact" added (used in lambdadelta)
47 files changed:
matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
matita/matita/contribs/lambdadelta/basic_2/computation/fprs.ma
matita/matita/contribs/lambdadelta/basic_2/computation/lfprs.ma
matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma
matita/matita/contribs/lambdadelta/basic_2/computation/tprs.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpr.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpr_ssta.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_dxprs.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_ssta.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs.ma
matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs.ma
matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfpcs.ma
matita/matita/contribs/lambdadelta/basic_2/unfold/ldrops.ma
matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
matita/matita/lib/lambda/background/preamble.ma
matita/matita/lib/lambda/paths/alternative_standard_order.ma
matita/matita/lib/lambda/paths/decomposed_trace.ma
matita/matita/lib/lambda/paths/dst_computation.ma
matita/matita/lib/lambda/paths/labeled_sequential_computation.ma
matita/matita/lib/lambda/paths/labeled_sequential_reduction.ma
matita/matita/lib/lambda/paths/labeled_st_computation.ma
matita/matita/lib/lambda/paths/labeled_st_reduction.ma
matita/matita/lib/lambda/paths/path.ma
matita/matita/lib/lambda/paths/standard_order.ma
matita/matita/lib/lambda/paths/standard_precedence.ma
matita/matita/lib/lambda/paths/standard_trace.ma
matita/matita/lib/lambda/paths/trace.ma
matita/matita/lib/lambda/subterms/boolean.ma
matita/matita/lib/lambda/subterms/booleanized.ma
matita/matita/lib/lambda/subterms/carrier.ma
matita/matita/lib/lambda/subterms/relocating_substitution.ma
matita/matita/lib/lambda/subterms/relocation.ma
matita/matita/lib/lambda/subterms/subterms.ma
matita/matita/lib/lambda/terms/labeled_sequential_computation.ma
matita/matita/lib/lambda/terms/multiplicity.ma
matita/matita/lib/lambda/terms/parallel_computation.ma
matita/matita/lib/lambda/terms/parallel_reduction.ma
matita/matita/lib/lambda/terms/relocating_substitution.ma
matita/matita/lib/lambda/terms/relocation.ma
matita/matita/lib/lambda/terms/sequential_computation.ma
matita/matita/lib/lambda/terms/sequential_reduction.ma
matita/matita/lib/lambda/terms/size.ma
matita/matita/lib/lambda/terms/term.ma
matita/matita/matita.lang