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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Thu, 16 Apr 2020 16:13:01 +0000 (18:13 +0200)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 18 Apr 2020 11:43:38 +0000 (13:43 +0200)
commit	3c7b4071a9ac096b02334c1d47468776b948e2de
tree	c44da9758331c2ecc9ec0df7f61f761de5e8db18	tree \| snapshot
parent	2f6f2b7c01d47d23f61dd48d767bcb37aecdcfea	commit \| diff

milestone update in basic_2, update in ground and static_2

+ new definition of cpx and derivatives without the sort hierarchy parameter
+ sort hierarchy parameter removed from ex_fpbg_refl.ma

187 files changed:

matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx_trans.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_teqx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_teqx_conf.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpmuwe.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_fsb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubty_6.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubty_7.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtyproper_6.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtyproper_7.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystar_6.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystar_7.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystarproper_6.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystarproper_7.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystrong_3.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsubtystrong_4.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_4.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_5.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predty_7.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtynormal_3.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtynormal_4.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysn_3.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysn_4.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysn_5.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_3.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_4.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_3.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_4.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystar_4.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystar_5.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_3.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_4.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/topredtysnstrong_3.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/topredtysnstrong_4.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmre_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprre_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_ext.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_feqx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lsubr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_reqx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo_vector.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_feqx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fpb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_feqx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_jsx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_lsubr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_rsx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_feqx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_reqx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_fqup.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_length.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_lpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_rsx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_simple.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_lsubr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_cpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops_basic.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ext.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_feqx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_reqx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_simple.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbq_fpb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_fquq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_fsle.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_length.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_reqx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_drops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fqup.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_length.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_lpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_rpx.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
matita/matita/contribs/lambdadelta/ground/lib/arith.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/lib/relations.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/steps/rtc.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt_max.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/i_static/rexs_lex.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/fsle_fsle.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/rex.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/rex_fsle.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/static/rex_lex.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/sh.ma		diff \| blob \| history

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

RSS Atom