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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 18 Apr 2014 19:09:54 +0000 (19:09 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 18 Apr 2014 19:09:54 +0000 (19:09 +0000)
commit	f282b35b958c9602fb1f47e5677b5805a046ac76
tree	279599f1fee440f6f91f1052d04beec39b887d99	tree \| snapshot
parent	cb5ca7ea4e826e9331eabeaea44353caab00071e	commit \| diff

- the relation for pointwise extensions now takes a binder as argument
- explicit alternative definition of lprs and lpxs removed
- changes in the notation for subclosures and refinements

80 files changed:

matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_alt.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_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/lsubc.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/notation.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_2.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_4.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqa_3.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqd_5.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_3.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_5.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/supterm_6.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermopt_6.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermoptalt_6.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermplus_6.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/suptermstar_6.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/fquq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_lpx_sn.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_tc.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_alt.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_lpx_sn.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_tc.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/aaa_fqus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/lsuba_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/lsubd.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/lsubd_da.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/lsubr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/lsubr_lsubr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/ssta_llpx_sn.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_alt.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma		diff \| 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

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

RSS Atom