]> matita.cs.unibo.it Git - helm.git/commit
bug fix in the notation of normal forms, now we specify that they are
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 29 Jan 2014 18:55:32 +0000 (18:55 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 29 Jan 2014 18:55:32 +0000 (18:55 +0000)
commit606dab57f31b66eb3f30f603185124b88dfad4c1
tree3551db7c0b05928c7e0421b08e6db33fcc9267db
parent946abd88fa24966751555193b0fe0d52e50722f2
bug fix in the notation of normal forms, now we specify that they are
normal forms for reduction. This will allow to enable normal forms for
substitution ...
39 files changed:
matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma
matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma
matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma
matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_3.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_3.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_3.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_5.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cix_append.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/crr_append.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl