]> matita.cs.unibo.it Git - helm.git/commit
- cprs and cnx on the way
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 16 Feb 2017 11:22:04 +0000 (11:22 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 16 Feb 2017 11:22:04 +0000 (11:22 +0000)
commit2002da6bcdbf12203a87a7d9630d738f67ede68c
tree19fc685f539430044b0b893c965c4fc64dd54a6d
parenta5a7eb39b9bad97d52d836ad1401329cff5b58a3
- cprs and cnx on the way
- breaks repositioning in notation
- corrections in NF and SN
- refactoring
61 files changed:
matita/matita/contribs/lambdadelta/basic_2/etc/cnx/cnx.etc
matita/matita/contribs/lambdadelta/basic_2/etc/cnx/cnx_lift.etc [deleted file]
matita/matita/contribs/lambdadelta/basic_2/etc/cnx/prednormal_5.etc [deleted file]
matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/etc/notation/prednormal_5.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/notation/relations/atomicarity_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_8.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredalt_8.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_8.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_8.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstaralt_8.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_8.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_7.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_3.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/ineint_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqc_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqf_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_7.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtynormal_5.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysn_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystar_5.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_5.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/supterm_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermopt_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermplus_6.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermstar_6.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_simple.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt
matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
matita/matita/contribs/lambdadelta/ground_2/lib/star.ma
matita/matita/contribs/lambdadelta/hls.ml [new file with mode: 0644]