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

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

2012-05-17	Andrea Asperti	filtering on a list without repetitions	tree \| commitdiff
2012-05-17	Wilmer Ricciotti	Added null character.	tree \| commitdiff
2012-05-16	Claudio Sacerdoti...	Removed duplicated notation and interaction with the...	tree \| commitdiff
2012-05-16	Claudio Sacerdoti...	Added alias instance=1 to avoid interaction with the...	tree \| commitdiff
2012-05-16	Andrea Asperti	a bit more	tree \| commitdiff
2012-05-15	Claudio Sacerdoti...	Patch by Ferruccio that enables \top/\bot for False...	tree \| commitdiff
2012-05-15	Wilmer Ricciotti	Progress	tree \| commitdiff
2012-05-15	Ferruccio Guidi	we added the standard notation for True and False ...	tree \| commitdiff
2012-05-15	Andrea Asperti	sempre li	tree \| commitdiff
2012-05-15	Wilmer Ricciotti	Added universal machine (mockup)	tree \| commitdiff
2012-05-14	Wilmer Ricciotti	Added copy machine (mockup)	tree \| commitdiff
2012-05-14	Andrea Asperti	progresprogresss	tree \| commitdiff
2012-05-14	Andrea Asperti	almost there	tree \| commitdiff
2012-05-14	Andrea Asperti	progress	tree \| commitdiff
2012-05-11	Wilmer Ricciotti	Definition of the structure of the transition table...	tree \| commitdiff
2012-05-11	Andrea Asperti	poca roba	tree \| commitdiff
2012-05-11	Andrea Asperti	restructuring	tree \| commitdiff
2012-05-11	Wilmer Ricciotti	Finished wsem_compare proof.	tree \| commitdiff
2012-05-11	Andrea Asperti	progress	tree \| commitdiff
2012-05-10	Wilmer Ricciotti	Progress.	tree \| commitdiff
2012-05-10	Wilmer Ricciotti	Progress.	tree \| commitdiff
2012-05-10	Ferruccio Guidi	- lib: some additions	tree \| commitdiff
2012-05-10	Andrea Asperti	axiomatization of acc_if	tree \| commitdiff
2012-05-09	Wilmer Ricciotti	Progress.	tree \| commitdiff
2012-05-09	Wilmer Ricciotti	Progress in compare.ma (some machines have been moved...	tree \| commitdiff
2012-05-08	Wilmer Ricciotti	progress in turing/universal/compare.ma	tree \| commitdiff
2012-05-08	Wilmer Ricciotti	Added compare auxiliary machine for universal turing...	tree \| commitdiff
2012-05-07	Wilmer Ricciotti	progress	tree \| commitdiff
2012-05-07	Andrea Asperti	Prove di terminazione	tree \| commitdiff
2012-05-07	Andrea Asperti	More examples	tree \| commitdiff
2012-05-07	Andrea Asperti	starl	tree \| commitdiff
2012-05-04	Wilmer Ricciotti	Forgotten in previous commit: move_char machines.	tree \| commitdiff
2012-05-04	Claudio Sacerdoti...	(no commit message)	tree \| commitdiff
2012-05-04	Claudio Sacerdoti...	(no commit message)	tree \| commitdiff
2012-05-04	Wilmer Ricciotti	Added a turing/universal directory for the universal...	tree \| commitdiff
2012-05-04	Wilmer Ricciotti	progress	tree \| commitdiff
2012-05-03	Wilmer Ricciotti	progress in while test machine	tree \| commitdiff
2012-05-03	Andrea Asperti	prod fin set	tree \| commitdiff
2012-05-03	Andrea Asperti	bool and segments of natural numbers	tree \| commitdiff
2012-05-02	Wilmer Ricciotti	While semantics.	tree \| commitdiff
2012-05-02	Andrea Asperti	split e merge	tree \| commitdiff
2012-05-02	Andrea Asperti	progress	tree \| commitdiff
2012-05-02	Andrea Asperti	while machine	tree \| commitdiff
2012-05-02	Wilmer Ricciotti	Added weak realizability.	tree \| commitdiff
2012-05-02	Andrea Asperti	Added wmono.	tree \| commitdiff
2012-04-30	Wilmer Ricciotti	More proofs in if-then-else machine.	tree \| commitdiff
2012-04-30	Andrea Asperti	Le configurazioni sono definite non su macchine ma...	tree \| commitdiff
2012-04-30	Andrea Asperti	Definition of accRealize	tree \| commitdiff
2012-04-30	Andrea Asperti	If machine	tree \| commitdiff
2012-04-30	Wilmer Ricciotti	Monotape turing machines update.	tree \| commitdiff
2012-04-27	Wilmer Ricciotti	more loop proofs	tree \| commitdiff
2012-04-27	Wilmer Ricciotti	loop functions	tree \| commitdiff
2012-04-27	Andrea Asperti	loop functions	tree \| commitdiff
2012-04-27	Andrea Asperti	Mono tape turing machines	tree \| commitdiff
2012-04-27	Andrea Asperti	Extensions to finset (sum) and auxiliary lemmas.	tree \| commitdiff
2012-04-26	Ferruccio Guidi	- notation (possibly affecting all .ma files):	tree \| commitdiff
2012-04-25	Ferruccio Guidi	- lambda_delta: bug fix in static type assignment	tree \| commitdiff
2012-04-24	Wilmer Ricciotti	Update to universal turing machine (preliminaries).	tree \| commitdiff
2012-04-24	Wilmer Ricciotti	More turing machines (still not compiling)	tree \| commitdiff
2012-04-24	Wilmer Ricciotti	Started converting informal definition of the machines...	tree \| commitdiff
2012-04-23	Wilmer Ricciotti	Added universal turing machines (only comments for...	tree \| commitdiff
2012-04-21	Ferruccio Guidi	- lambda_delta: static type assignment is defined	tree \| commitdiff
2012-04-13	Andrea Asperti	Definition of complexity	tree \| commitdiff
2012-04-04	Andrea Asperti	Added in basics	tree \| commitdiff
2012-03-23	Ferruccio Guidi	- pts: we restored the former hierarchy	tree \| commitdiff
2012-03-19	Ferruccio Guidi	- basics: bug fix in Conf3, it was not generic enough	tree \| commitdiff
2012-03-17	Ferruccio Guidi	- basics: some support for abstract triangular confluen...	tree \| commitdiff
2012-03-15	Ferruccio Guidi	- lambda_delta: strong normalization of simply typed...	tree \| commitdiff
2012-03-09	Ferruccio Guidi	- lambda_delta: morew propertie in context-sensitive...	tree \| commitdiff
2012-03-08	Andrea Asperti	Axiom proved	tree \| commitdiff
2012-03-04	Ferruccio Guidi	- lambda_delta: "conversion" and "equivalence" componen...	tree \| commitdiff
2012-01-31	Claudio Sacerdoti...	Notation for destructuring let-in for triples fixed.	tree \| commitdiff
2012-01-10	Andrea Asperti	A complete snapshot for re	tree \| commitdiff
2012-01-07	Ferruccio Guidi	lambda_delta: global environments handling: redefined...	tree \| commitdiff
2012-01-03	Andrea Asperti	Complete version	tree \| commitdiff
2012-01-03	Andrea Asperti	modified definition of memb	tree \| commitdiff
2012-01-03	Andrea Asperti	reverse	tree \| commitdiff
2012-01-03	Andrea Asperti	more properties of union	tree \| commitdiff
2012-01-03	Andrea Asperti	noteq_to_eqnot	tree \| commitdiff
2011-12-20	Ferruccio Guidi	- the definition of the framework for strong normalizat...	tree \| commitdiff
2011-12-15	Andrea Asperti	Splitted DeqSets in their own file. Notation for memb...	tree \| commitdiff
2011-12-15	Andrea Asperti	Hints sui DeqSets	tree \| commitdiff
2011-12-14	Claudio Sacerdoti...	More stuff from CerCo to the standard library.	tree \| commitdiff
2011-12-14	Claudio Sacerdoti...	Some more lemmas from CerCo.	tree \| commitdiff
2011-12-14	Claudio Sacerdoti...	1) Notation for dependent pairs differentiated from...	tree \| commitdiff
2011-12-13	Claudio Sacerdoti...	Dependent pairs (i.e. Sigma types in Type[0]) are back...	tree \| commitdiff
2011-12-13	Claudio Sacerdoti...	1) PSig and Sig merged into a single Sigma type in...	tree \| commitdiff
2011-12-13	Claudio Sacerdoti...	inject/eject replaced by mk_Sig/pi1.	tree \| commitdiff
2011-12-13	Claudio Sacerdoti...	1) New file russell with the coercions to activate...	tree \| commitdiff
2011-12-13	Andrea Asperti	Splitted re into lang.ma nd re.ma	tree \| commitdiff
2011-12-13	Andrea Asperti	Sig in Prop	tree \| commitdiff
2011-12-13	Claudio Sacerdoti...	More stuff integrated from CerCo on sigma types (that...	tree \| commitdiff
2011-12-12	Claudio Sacerdoti...	pair => mk_Prod (one more was left in notation)	tree \| commitdiff
2011-12-12	Claudio Sacerdoti...	precedence level of if-then-else fixed	tree \| commitdiff
2011-12-12	Claudio Sacerdoti...	Added elimination principles for destructuring let...	tree \| commitdiff
2011-12-12	Claudio Sacerdoti...	Some integrations from CerCo. In particular:	tree \| commitdiff
2011-12-12	Claudio Sacerdoti...	Pairs are now records.	tree \| commitdiff
2011-12-12	Claudio Sacerdoti...	Parentheses are now needed. I do not know why and when...	tree \| commitdiff
2011-12-12	Ferruccio Guidi	nat library reorganized ....	tree \| commitdiff
2011-12-12	Andrea Asperti	Generalization to any alphabet. We do not need a finite	tree \| commitdiff
next

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

RSS Atom