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

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

[helm.git] / helm / software / matita / nlibrary /

2011-01-21	Wilmer Ricciotti	Removed inclusion of logic/equality.ma in datatypes...	tree \| commitdiff
2010-12-22	Wilmer Ricciotti	more theory for lists	tree \| commitdiff
2010-12-22	Wilmer Ricciotti	...	tree \| commitdiff
2010-10-17	Enrico Tassi	fixed many scripts that broke for various reasons	tree \| commitdiff
2010-10-01	Enrico Tassi	16.2	tree \| commitdiff
2010-09-30	Enrico Tassi	...	tree \| commitdiff
2010-09-29	Enrico Tassi	hints for \epsilon	tree \| commitdiff
2010-09-28	Enrico Tassi	hints polished and fixed to allow recursive inference...	tree \| commitdiff
2010-09-28	Enrico Tassi	nicer hints, 16.1->3 done	tree \| commitdiff
2010-09-27	Enrico Tassi	many fixes to setoids for re, 16.1 almost done	tree \| commitdiff
2010-09-25	Enrico Tassi	some reorganization + some more re-setoids.ma proofs	tree \| commitdiff
2010-09-23	Enrico Tassi	morphism support moved to sets/ and logic/cprop	tree \| commitdiff
2010-09-23	Enrico Tassi	interpretation for <->	tree \| commitdiff
2010-09-23	Enrico Tassi	fix typo	tree \| commitdiff
2010-09-23	Enrico Tassi	Setoid-Rewriting under Ex works for an arbitrary depth...	tree \| commitdiff
2010-09-16	Enrico Tassi	fixed notation	tree \| commitdiff
2010-09-12	Enrico Tassi	some more work	tree \| commitdiff
2010-09-12	Enrico Tassi	Change (or better define) the order of hints premises.	tree \| commitdiff
2010-09-12	Enrico Tassi	non uniform coercions landed in hints_declaration.ma...	tree \| commitdiff
2010-09-09	Enrico Tassi	Some refactoring in set*.ma, some new notations and...	tree \| commitdiff
2010-09-09	Enrico Tassi	th 16.2 proved in the setoids setting	tree \| commitdiff
2010-09-08	Enrico Tassi	...	tree \| commitdiff
2010-09-08	Enrico Tassi	...	tree \| commitdiff
2010-09-08	Enrico Tassi	...	tree \| commitdiff
2010-09-08	Enrico Tassi	...	tree \| commitdiff
2010-07-28	Claudio Sacerdoti...	...	tree \| commitdiff
2010-07-23	Claudio Sacerdoti...	Some experiments on a co-inductive Heityng algebra.	tree \| commitdiff
2010-07-22	Enrico Tassi	some work on \exists	tree \| commitdiff
2010-07-22	Enrico Tassi	eq -> eq0 renaming	tree \| commitdiff
2010-07-22	Enrico Tassi	fixed precedence so that no () are needed around variab...	tree \| commitdiff
2010-07-21	Enrico Tassi	...	tree \| commitdiff
2010-07-21	Enrico Tassi	...	tree \| commitdiff
2010-07-21	Enrico Tassi	...	tree \| commitdiff
2010-07-21	Enrico Tassi	...	tree \| commitdiff
2010-07-20	Enrico Tassi	completed lemma 17	tree \| commitdiff
2010-07-19	Enrico Tassi	...	tree \| commitdiff
2010-07-15	Enrico Tassi	re 16.4 almost done	tree \| commitdiff
2010-07-07	Enrico Tassi	moved formal_topology into library"	tree \| commitdiff
2010-06-07	Enrico Tassi	some stuff on re	tree \| commitdiff
2010-05-12	Wilmer Ricciotti	Library support files for John Major equality and Russell.	tree \| commitdiff
2010-05-11	Andrea Asperti	minimization.ma	tree \| commitdiff
2010-05-10	Enrico Tassi	new intro:	tree \| commitdiff
2010-05-07	Enrico Tassi	notation	tree \| commitdiff
2010-05-06	Claudio Sacerdoti...	...	tree \| commitdiff
2010-05-05	Claudio Sacerdoti...	coinduction is between us	tree \| commitdiff
2010-05-05	Claudio Sacerdoti...	First tests.	tree \| commitdiff
2010-05-04	Claudio Sacerdoti...	Regular expressions.	tree \| commitdiff
2010-04-21	Ferruccio Guidi	new dependences	tree \| commitdiff
2010-04-15	Enrico Tassi	bool_ext on 'o' not on 'Prop' (they are convertible...	tree \| commitdiff
2010-04-14	Claudio Sacerdoti...	...	tree \| commitdiff
2010-04-14	Claudio Sacerdoti...	...	tree \| commitdiff
2010-04-14	Claudio Sacerdoti...	Formal points.	tree \| commitdiff
2010-04-14	Claudio Sacerdoti...	Some dualization clean-up.	tree \| commitdiff
2010-04-13	Enrico Tassi	fixed support file for TPTP	tree \| commitdiff
2010-04-08	Enrico Tassi	...	tree \| commitdiff
2010-03-31	Claudio Sacerdoti...	Not is now inductive.	tree \| commitdiff
2010-03-31	Claudio Sacerdoti...	Use the inversion!	tree \| commitdiff
2010-03-31	Andrea Asperti	removed boh	tree \| commitdiff
2010-03-26	Claudio Sacerdoti...	Good definition found.	tree \| commitdiff
2010-03-26	Claudio Sacerdoti...	(Co)Inductively Generated Formal Topologies (not only...	tree \| commitdiff
2010-03-25	Matthias Puech	patched the definition of locate, advances in locate_ad...	tree \| commitdiff
2010-03-25	Wilmer Ricciotti	Z.ma updated to reflect changes in the logical Not...	tree \| commitdiff
2010-03-25	Matthias Puech	Automation problem	tree \| commitdiff
2010-03-25	Andrea Asperti	More work	tree \| commitdiff
2010-03-25	Andrea Asperti	cosi va (se vi pare).	tree \| commitdiff
2010-03-25	Claudio Sacerdoti...	...	tree \| commitdiff
2010-03-25	Andrea Asperti	Conflict(?).	tree \| commitdiff
2010-03-24	Claudio Sacerdoti...	Nice examples for automation (that fails).	tree \| commitdiff
2010-03-24	Claudio Sacerdoti...	Simplified proof after pattern fix	tree \| commitdiff
2010-03-24	Claudio Sacerdoti...	"Not" is no longer a definition	tree \| commitdiff
2010-03-24	Claudio Sacerdoti...	The precedence of ^-1 has changed.	tree \| commitdiff
2010-03-24	Claudio Sacerdoti...	Real numbers as co-inductive streams of digits (overlap...	tree \| commitdiff
2010-03-23	Matthias Puech	typo in a proof	tree \| commitdiff
2010-03-23	Andrea Asperti	One more case.	tree \| commitdiff
2010-03-23	Andrea Asperti	Readded eqf_2.	tree \| commitdiff
2010-03-23	Andrea Asperti	symmetric_eq -> sym_eq	tree \| commitdiff
2010-03-23	Andrea Asperti	Re-proved an axiom	tree \| commitdiff
2010-03-23	Andrea Asperti	Commented a few lemmas (copies).	tree \| commitdiff
2010-03-23	Andrea Asperti	Keeping only lift_aux e subst_aux (renamed to lift...	tree \| commitdiff
2010-03-23	Andrea Asperti	Moved compare in a different file.	tree \| commitdiff
2010-03-18	Andrea Asperti	Porting alla nuova def. di negazione	tree \| commitdiff
2010-03-18	Andrea Asperti	Nuova versione di not.	tree \| commitdiff
2010-03-18	Andrea Asperti	Porting the new definition of equality.	tree \| commitdiff
2010-03-17	Andrea Asperti	qualche caso del lemma 5.2.11	tree \| commitdiff
2010-03-17	Andrea Asperti	Splitted gpts in two files.	tree \| commitdiff
2010-03-17	Andrea Asperti	Aggiornamento alla negazione.	tree \| commitdiff
2010-03-17	Andrea Asperti	Nuova definizione della negazione.	tree \| commitdiff
2010-03-16	Claudio Sacerdoti...	...	tree \| commitdiff
2010-03-12	Andrea Asperti	First version of PTS	tree \| commitdiff
2010-03-12	Andrea Asperti	New definition of negation	tree \| commitdiff
2010-03-02	Wilmer Ricciotti	Added reverse rewriting principle in Type[0].	tree \| commitdiff
2010-03-02	Wilmer Ricciotti	Some integrations to the ng library.	tree \| commitdiff
2010-02-19	Andrea Asperti	New proofs.	tree \| commitdiff
2010-02-19	Andrea Asperti	Wilmer's stuff for destruct.	tree \| commitdiff
2010-02-19	Andrea Asperti	(no commit message)	tree \| commitdiff
2010-02-16	Andrea Asperti	More theorems	tree \| commitdiff
2010-02-16	Andrea Asperti	Minor fixings.	tree \| commitdiff
2010-02-11	Enrico Tassi	minimal sequent height set to 1	tree \| commitdiff
2010-02-11	Enrico Tassi	some experiment filtering with height	tree \| commitdiff
2010-02-10	Andrea Asperti	addenda	tree \| commitdiff
next

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

RSS Atom