matita.cs.unibo.it Git - helm.git/history - helm/software/matita/contribs/POPLmark/Fsub

]> matita.cs.unibo.it Git - helm.git/history - helm/software/matita/contribs/POPLmark/Fsub

[helm.git] / helm / software / matita / contribs / POPLmark / Fsub /

2009-07-09	Wilmer Ricciotti	More updates to Fsub.	tree \| commitdiff
2009-06-19	Wilmer Ricciotti	More improvements.	tree \| commitdiff
2009-06-05	Wilmer Ricciotti	- replaced part1a/defn with the version based on induct...	tree \| commitdiff
2009-06-03	Wilmer Ricciotti	Update, using induction/inversion.	tree \| commitdiff
2009-06-01	Andrea Asperti	This works for me	tree \| commitdiff
2009-05-29	Wilmer Ricciotti	POPLmark part 1a using the de Bruijn encoding.	tree \| commitdiff
2009-05-25	Enrico Tassi	nasty change in the lexer/parser:	tree \| commitdiff
2009-05-13	Andrea Asperti	Via un'altra linea...	tree \| commitdiff
2009-05-13	Andrea Asperti	Sempre piu' breve	tree \| commitdiff
2009-05-11	Andrea Asperti	More automation	tree \| commitdiff
2009-04-28	Enrico Tassi	huge commit in automation:	tree \| commitdiff
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductiv...	tree \| commitdiff
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductiv...	tree \| commitdiff
2008-05-02	Wilmer Ricciotti	Some destruct tactics got broken after last update...	tree \| commitdiff
2008-04-24	Wilmer Ricciotti	Proof of adequacy.	tree \| commitdiff
2008-04-21	Claudio Sacerdoti...	defn2.ma is to be used with part1a_inversion3	tree \| commitdiff
2008-04-20	Claudio Sacerdoti...	Alternative prove using just one induction/inversion...	tree \| commitdiff
2008-04-18	Claudio Sacerdoti...	Dead code removed.	tree \| commitdiff
2008-04-18	Claudio Sacerdoti...	Inversion lemma for Forall.	tree \| commitdiff
2008-03-26	Wilmer Ricciotti	Reorganization of list library (step 1)	tree \| commitdiff
2008-03-23	Enrico Tassi	Fsub moved in contribs	tree \| commitdiff

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

RSS Atom