matita.cs.unibo.it Git - helm.git/commit - matita/matita/contribs/lambda/delifting

]> matita.cs.unibo.it Git - helm.git/commit - matita/matita/contribs/lambda/delifting_substitution.ma

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Thu, 6 Dec 2012 16:10:57 +0000 (16:10 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Thu, 6 Dec 2012 16:10:57 +0000 (16:10 +0000)
commit	cdcfe9f97936f02dab1970ebf3911940bf0a4e29
tree	02bbc737c6a66b1d9a9df6bbd9d0c9f5b276d131	tree \| snapshot
parent	4063c155ff95d3364fcdefb162f24d76b12c71a4	commit \| diff

- we enabled a notation for ex2
- we improved star_ind_l that now behaves as if starl were defined
with a "left parameter" occurring on the right. this makes star_ind_l
symmetric with respect to star_ind
- we commented the non-more-compiling sections of "turing"
- some progress in "lambda"

38 files changed:

matita/matita/contribs/lambda/delifting_substitution.ma		diff \| blob \| history
matita/matita/contribs/lambda/hap_computation.ma	[deleted file]	blob \| history
matita/matita/contribs/lambda/hap_reduction.ma	[deleted file]	blob \| history
matita/matita/contribs/lambda/labelled_hap_computation.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda/labelled_hap_reduction.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambda/labelled_sequential_computation.ma		diff \| blob \| history
matita/matita/contribs/lambda/labelled_sequential_reduction.ma		diff \| blob \| history
matita/matita/contribs/lambda/lift.ma		diff \| blob \| history
matita/matita/contribs/lambda/parallel_reduction.ma		diff \| blob \| history
matita/matita/contribs/lambda/policy.txt		diff \| blob \| history
matita/matita/contribs/lambda/preamble.ma		diff \| blob \| history
matita/matita/contribs/lambda/redex_pointer.ma		diff \| blob \| history
matita/matita/contribs/lambda/redex_pointer_sequence.ma		diff \| blob \| history
matita/matita/contribs/lambda/st_computation.ma		diff \| blob \| history
matita/matita/contribs/lambda/term.ma		diff \| blob \| history
matita/matita/contribs/lambda/xoa.conf.xml		diff \| blob \| history
matita/matita/contribs/lambda/xoa.ma		diff \| blob \| history
matita/matita/contribs/lambda/xoa_notation.ma		diff \| blob \| history
matita/matita/lib/basics/core_notation.ma		diff \| blob \| history
matita/matita/lib/basics/lists/list.ma		diff \| blob \| history
matita/matita/lib/basics/logic.ma		diff \| blob \| history
matita/matita/lib/basics/star.ma		diff \| blob \| history
matita/matita/lib/turing/complexity.ma		diff \| blob \| history
matita/matita/lib/turing/move_char.ma		diff \| blob \| history
matita/matita/lib/turing/multi_universal/compare.ma		diff \| blob \| history
matita/matita/lib/turing/multi_universal/copy.ma		diff \| blob \| history
matita/matita/lib/turing/multi_universal/match.ma		diff \| blob \| history
matita/matita/lib/turing/multi_universal/moves.ma		diff \| blob \| history
matita/matita/lib/turing/ntm.ma		diff \| blob \| history
matita/matita/lib/turing/oracle.ma		diff \| blob \| history
matita/matita/lib/turing/turing_old.ma		diff \| blob \| history
matita/matita/lib/turing/universal.ma		diff \| blob \| history
matita/matita/lib/turing/universal/copy.ma		diff \| blob \| history
matita/matita/lib/turing/universal/marks.ma		diff \| blob \| history
matita/matita/lib/turing/universal/match_machines.ma		diff \| blob \| history
matita/matita/lib/turing/universal/uni_step.ma		diff \| blob \| history
matita/matita/lib/turing/universal/universal.ma		diff \| blob \| history
matita/matita/lib/turing/wmono.ma		diff \| blob \| history

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

RSS Atom