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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Tue, 11 Mar 2014 17:57:05 +0000 (17:57 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Tue, 11 Mar 2014 17:57:05 +0000 (17:57 +0000)
commit	8a5a354c9ac3ef20ca01dbeb61f6b99902f172a7
tree	eefbe486747fc07c86d8dd39d75544054e59c1c9	tree \| snapshot
parent	4e2cde56d7a4c30c1fa07d58f76beab22a174151	commit \| diff

reaxiomatized lleq fixes a bug in it and allows to park substitution in etc

70 files changed:

matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_leq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fpns.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpx_cpys.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpxs_cpys.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpy.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpy_cpy.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpy_lift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys_alt.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys_cpys.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys_lift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/extlrsubeq_4.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lazyeqalt_4.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_alt.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_ext.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_fqus.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_ldrop.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_lleq.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lpx_cpys.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lsuby.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lsuby_lsuby.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/psubst_6.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/psubststar_6.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/psubststaralt_6.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/extlrsubeq_4.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqalt_4.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubst_6.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststar_6.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststaralt_6.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_leq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_cpys.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_lleq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_lleq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_ldrop.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_ldrop.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby_lsuby.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_lleq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_lleq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma	[deleted file]	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