matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Tue, 16 Apr 2013 19:45:41 +0000 (19:45 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Tue, 16 Apr 2013 19:45:41 +0000 (19:45 +0000)
commit	713673ecf863cb6187291f016ed4490b12a03ac0
tree	4a830c806bb4bf9ae61bd4eae6339c68c5abeb03	tree \| snapshot
parent	520d4370a540a98f5e5e1d85acfef0c982cc1e04	commit \| diff

- we commit just the components before "reducibility"
- reaxiomatized substitution and reduction now commute with respect to
subclosure
- delift and thin removed for now

92 files changed:

matita/matita/contribs/lambdadelta/basic_2/etc/cpr/aaa_ltpss_dx.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/aaa_ltpss_sn.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/cpr_lift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpr.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpr_ldrop.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpr_ltpr.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpss_dx.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpss_dx_ldrop.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpss_dx_ltpss_dx.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpss_dx_tps.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpss_dx_tpss.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpss_sn.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpss_sn_alt.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpss_sn_ldrop.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpss_sn_ltpss_sn.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpss_sn_tps.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltpss_sn_tpss.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ssta_ltpss_dx.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ssta_ltpss_sn.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/sstas_ltpss_dx.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/sstas_ltpss_sn.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpr.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpr_lift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpr_tpr.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tps.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tps_lift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tps_tps.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpss.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpss_alt.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpss_lift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpss_tpss.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_alt.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_delift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_lift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_ltpss.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/delift/delift_tpss.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/delift/thin.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/delift/thin_delift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/delift/thin_ldrop.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/fsup/fsups_fsups.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/restricted/cpqs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/restricted/lpqs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/restricted/lpqs_cpqs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/restricted/lpqs_lpqs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/aaa_lpss.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/static/aaa_ltpss_dx.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/aaa_ltpss_sn.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/ssta_lpss.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_dx.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_sn.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/tps_tps.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/delift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/delift_delift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/delift_ltpss.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/delift_tpss.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/fsups.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/unfold/fsups_fsups.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/unfold/lpss.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_cpss.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ldrop.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ltpss_dx.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tps.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tpss.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ltpss_sn.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tps.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_tpss.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/thin.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/thin_delift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/thin_ldrop.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_lift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_tpss.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lpss.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_dx.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_sn.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl		diff \| blob \| history
matita/matita/predefined_virtuals.ml		diff \| blob \| history

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom