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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 23 Aug 2019 19:24:02 +0000 (21:24 +0200)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 23 Aug 2019 19:24:02 +0000 (21:24 +0200)
commit	bac74b5cff042d37e1abc9c961a6c41094b8a294
tree	c5a99a7795460a7b846bb571501e9d1687280c9f	tree \| snapshot
parent	cacd7323994f7621286dbfd93bbf4c50acfbe918	commit \| diff

update in ground_2 static_2 basic_2

+ the applicability parameter is now a predicate
+ tueq removed in favor of theq
+ two conjectures to prove ...

72 files changed:

matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.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_cpmhe.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpue.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_eval.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cnu.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cnu_cnr.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cnu_cnr_simple.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cnu_cnu.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cnu_drops.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cnu_lifts.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cnu_tdeq.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cnv_cpmue.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cnv_cpue.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cpm_tueq.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cpms_cnu.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cpmue.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cpmue_csx.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cpue.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cpue_csx.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpue/prediteval_5.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/predevalstar_6.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/prediteval_5.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmhe.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmhe_csx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cnh.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cnu.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpue.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpue_csx.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_cpes.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_cpms.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_cprs.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_cnh.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_drops.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_lifts.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_simple.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnh_tdeq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnr.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnr_simple.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_cnu.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_drops.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_lifts.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnu_tdeq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tueq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/etc/tueq/approxeq_2.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/etc/tueq/lifts_tueq.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/etc/tueq/tueq.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/etc/tueq/tueq_tueq.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/notation/relations/approxeq_2.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/relocation/lifts_theq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tueq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/syntax/tueq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/syntax/tueq_tueq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl		diff \| blob \| history

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

RSS Atom