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

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

author	Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
	Thu, 30 Dec 2021 12:24:12 +0000 (13:24 +0100)
committer	Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
	Thu, 30 Dec 2021 12:24:12 +0000 (13:24 +0100)
commit	873fb39bdd21aa14877bf5d50db26e3a050c6d43
tree	08431372b95202c6253ccaf0b38d83df13a5d87c	tree \| snapshot
parent	503500ff9a6d9cca363a42b5fe7f3f5de69239f9	commit \| diff

update in ground, static_2 and apps_2

+ updated notation for extensional equality

50 files changed:

matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_vlift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/apps_2/models/tm_vpush.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/nat_succ_iter.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/lib/exteq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/notation/relations/circled_eq_4.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_2.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/ground/notation/relations/doteq_4.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/notation/relations/epsilon_3.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/notation/relations/ideq_2.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after_ist.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_after_isi.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist_isi.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_isi.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_eq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_id_eq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_isd_eq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_eq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_id.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_uni.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_isu_uni.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_nexts_eq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_id.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_tls.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_pushs_eq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_eq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isi.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_sor.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq_eq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_eq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_nexts_eq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_tls_pushs_eq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/pr_uni_eq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/relocation/tr_eq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl		diff \| blob \| history
matita/matita/contribs/lambdadelta/static_2/notation/relations/ideq_2.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/static_2/syntax/teq.ma		diff \| blob \| history
matita/matita/predefined_virtuals.ml		diff \| blob \| history

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

RSS Atom