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

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

2012-01-08	Ferruccio Guidi	- notation restyling ...	commit \| commitdiff \| tree \| snapshot
2012-01-07	Ferruccio Guidi	Basic_2: - we addedsome files	commit \| commitdiff \| tree \| snapshot
2012-01-07	Ferruccio Guidi	lambda_delta: global environments handling: redefined...	commit \| commitdiff \| tree \| snapshot
2012-01-04	Ferruccio Guidi	the support for reducibility candidates evolves ,,,,	commit \| commitdiff \| tree \| snapshot
2012-01-03	Andrea Asperti	Complete version	commit \| commitdiff \| tree \| snapshot
2012-01-03	Andrea Asperti	modified definition of memb	commit \| commitdiff \| tree \| snapshot
2012-01-03	Andrea Asperti	reverse	commit \| commitdiff \| tree \| snapshot
2012-01-03	Andrea Asperti	more properties of union	commit \| commitdiff \| tree \| snapshot
2012-01-03	Andrea Asperti	noteq_to_eqnot	commit \| commitdiff \| tree \| snapshot
2011-12-26	Ferruccio Guidi	notation and dependences bug fix	commit \| commitdiff \| tree \| snapshot
2011-12-25	Ferruccio Guidi	Basic 2 page update	commit \| commitdiff \| tree \| snapshot
2011-12-25	Ferruccio Guidi	- support for candidates of reducibility continues ...	commit \| commitdiff \| tree \| snapshot
2011-12-20	Ferruccio Guidi	Basic_2 update ...	commit \| commitdiff \| tree \| snapshot
2011-12-20	Ferruccio Guidi	- the definition of the framework for strong normalizat...	commit \| commitdiff \| tree \| snapshot
2011-12-16	Andrea Asperti	In case paramodulation fails we apply unit equalities.	commit \| commitdiff \| tree \| snapshot
2011-12-15	Andrea Asperti	Splitted DeqSets in their own file. Notation for memb...	commit \| commitdiff \| tree \| snapshot
2011-12-15	Andrea Asperti	Hints sui DeqSets	commit \| commitdiff \| tree \| snapshot
2011-12-14	Claudio Sacerdoti...	More stuff from CerCo to the standard library.	commit \| commitdiff \| tree \| snapshot
2011-12-14	Claudio Sacerdoti...	Some more lemmas from CerCo.	commit \| commitdiff \| tree \| snapshot
2011-12-14	Wilmer Ricciotti	Matitaweb: large commit porting to the new Matita 0...	commit \| commitdiff \| tree \| snapshot
2011-12-14	Claudio Sacerdoti...	1) Notation for dependent pairs differentiated from...	commit \| commitdiff \| tree \| snapshot
2011-12-13	Claudio Sacerdoti...	Dependent pairs (i.e. Sigma types in Type[0]) are back...	commit \| commitdiff \| tree \| snapshot
2011-12-13	Claudio Sacerdoti...	1) PSig and Sig merged into a single Sigma type in...	commit \| commitdiff \| tree \| snapshot
2011-12-13	Claudio Sacerdoti...	inject/eject replaced by mk_Sig/pi1.	commit \| commitdiff \| tree \| snapshot
2011-12-13	Claudio Sacerdoti...	1) New file russell with the coercions to activate...	commit \| commitdiff \| tree \| snapshot
2011-12-13	matitaweb	Chapter 5 = re.ma ; chapter 6 = moves.ma	commit \| commitdiff \| tree \| snapshot
2011-12-13	matitaweb	New chapter 4	commit \| commitdiff \| tree \| snapshot
2011-12-13	Wilmer Ricciotti	Matitaweb: clicking buttons disables the GUI to prevent...	commit \| commitdiff \| tree \| snapshot
2011-12-13	Andrea Asperti	Splitted re into lang.ma nd re.ma	commit \| commitdiff \| tree \| snapshot
2011-12-13	Andrea Asperti	Sig in Prop	commit \| commitdiff \| tree \| snapshot
2011-12-13	Claudio Sacerdoti...	More stuff integrated from CerCo on sigma types (that...	commit \| commitdiff \| tree \| snapshot
2011-12-13	Enrico Tassi	axiom-	commit \| commitdiff \| tree \| snapshot
2011-12-12	Claudio Sacerdoti...	pair => mk_Prod (one more was left in notation)	commit \| commitdiff \| tree \| snapshot
2011-12-12	Claudio Sacerdoti...	precedence level of if-then-else fixed	commit \| commitdiff \| tree \| snapshot
2011-12-12	Claudio Sacerdoti...	Added elimination principles for destructuring let...	commit \| commitdiff \| tree \| snapshot
2011-12-12	Claudio Sacerdoti...	Some integrations from CerCo. In particular:	commit \| commitdiff \| tree \| snapshot
2011-12-12	Enrico Tassi	support -axiom to avoind indexing an axiom (since there...	commit \| commitdiff \| tree \| snapshot
2011-12-12	Ferruccio Guidi	- we improved and updated the generated web pages	commit \| commitdiff \| tree \| snapshot
2011-12-12	Claudio Sacerdoti...	Pairs are now records.	commit \| commitdiff \| tree \| snapshot
2011-12-12	Claudio Sacerdoti...	Parentheses are now needed. I do not know why and when...	commit \| commitdiff \| tree \| snapshot
2011-12-12	Wilmer Ricciotti	Matitaweb: changes to matitadaemon.ml to make it work...	commit \| commitdiff \| tree \| snapshot
2011-12-12	Wilmer Ricciotti	Matitaweb: added utility for conversion of user dbs...	commit \| commitdiff \| tree \| snapshot
2011-12-12	Claudio Sacerdoti...	Re-Ported to	commit \| commitdiff \| tree \| snapshot
2011-12-12	Wilmer Ricciotti	Matitaweb: secure SHA-256 encryption for passwords.	commit \| commitdiff \| tree \| snapshot
2011-12-12	matitaweb	commit by user andrea	commit \| commitdiff \| tree \| snapshot
2011-12-12	matitaweb	commit by user andrea	commit \| commitdiff \| tree \| snapshot
2011-12-12	matitaweb	commit by user andrea	commit \| commitdiff \| tree \| snapshot
2011-12-12	matitaweb	commit by user andrea	commit \| commitdiff \| tree \| snapshot
2011-12-12	Ferruccio Guidi	nat library reorganized ....	commit \| commitdiff \| tree \| snapshot
2011-12-12	Andrea Asperti	Generalization to any alphabet. We do not need a finite	commit \| commitdiff \| tree \| snapshot
2011-12-11	Ferruccio Guidi	- slicing relation for the global environment defined...	commit \| commitdiff \| tree \| snapshot
2011-12-09	Andrea Asperti	list.ma moved inside lists.	commit \| commitdiff \| tree \| snapshot
2011-12-09	Andrea Asperti	closing more axioms	commit \| commitdiff \| tree \| snapshot
2011-12-08	Ferruccio Guidi	updating the information on lambda_delta	commit \| commitdiff \| tree \| snapshot
2011-12-08	Ferruccio Guidi	Maietty suggested to change a paragraph on the devel...	commit \| commitdiff \| tree \| snapshot
2011-12-08	Ferruccio Guidi	Maietti suggested to replace a paragraph about the...	commit \| commitdiff \| tree \| snapshot
2011-12-07	Andrea Asperti	Closing some axioms...	commit \| commitdiff \| tree \| snapshot
2011-12-07	Andrea Asperti	\vee notation for boolean or	commit \| commitdiff \| tree \| snapshot
2011-12-06	Ferruccio Guidi	new files started ...	commit \| commitdiff \| tree \| snapshot
2011-12-06	Ferruccio Guidi	other addition to the standard library removed	commit \| commitdiff \| tree \| snapshot
2011-12-06	Ferruccio Guidi	we added a definition and a couple of lemmas	commit \| commitdiff \| tree \| snapshot
2011-12-06	Ferruccio Guidi	- support for atomic arities and candidates of reducibi...	commit \| commitdiff \| tree \| snapshot
2011-12-06	Wilmer Ricciotti	Grammar change: let corecs can take no arguments (and...	commit \| commitdiff \| tree \| snapshot
2011-12-06	Wilmer Ricciotti	Fixes a bug that overwrited the index of the recursive...	commit \| commitdiff \| tree \| snapshot
2011-12-06	Andrea Asperti	Listb contains some boolean functions over lists.	commit \| commitdiff \| tree \| snapshot
2011-12-06	Wilmer Ricciotti	Matitaweb:	commit \| commitdiff \| tree \| snapshot
2011-12-06	Andrea Asperti	naive sets (A-> Prop)	commit \| commitdiff \| tree \| snapshot
2011-12-05	Andrea Asperti	More properties of iff	commit \| commitdiff \| tree \| snapshot
2011-12-05	Andrea Asperti	Decidability of equality (draft)	commit \| commitdiff \| tree \| snapshot
2011-11-26	Ferruccio Guidi	component "reducibility" updated to new syntax!	commit \| commitdiff \| tree \| snapshot
2011-11-26	Ferruccio Guidi	component "unfold" updated to new syntax ...	commit \| commitdiff \| tree \| snapshot
2011-11-26	Ferruccio Guidi	component "substitution" updated to new syntax ...	commit \| commitdiff \| tree \| snapshot
2011-11-26	Ferruccio Guidi	- "grammar" component updated to new syntax ...	commit \| commitdiff \| tree \| snapshot
2011-11-25	Ferruccio Guidi	Ground_2 ported to new syntax ...	commit \| commitdiff \| tree \| snapshot
2011-11-25	Ferruccio Guidi	bugfix in clearing the replaced variable: a relocation...	commit \| commitdiff \| tree \| snapshot
2011-11-24	Ferruccio Guidi	Destruct: we warn about the substituted variable to...	commit \| commitdiff \| tree \| snapshot
2011-11-24	Ferruccio Guidi	- now destruct tries to clear the replaced variables...	commit \| commitdiff \| tree \| snapshot
2011-11-24	Enrico Tassi	fixed DESTDIR	commit \| commitdiff \| tree \| snapshot
2011-11-24	Enrico Tassi	fixed DESTDIR	commit \| commitdiff \| tree \| snapshot
2011-11-22	Claudio Sacerdoti...	Changes to disambiguation:	commit \| commitdiff \| tree \| snapshot
2011-11-21	Ferruccio Guidi	Basic_2 file names update	commit \| commitdiff \| tree \| snapshot
2011-11-21	Claudio Sacerdoti...	Syntax change: change where what => change what where.	commit \| commitdiff \| tree \| snapshot
2011-11-21	Andrea Asperti	regular expressions	commit \| commitdiff \| tree \| snapshot
2011-11-21	Andrea Asperti	Filtering all equations that cannot be embedded (contai...	commit \| commitdiff \| tree \| snapshot
2011-11-21	Andrea Asperti	Passing the correct subst a metasenv when idexing local...	commit \| commitdiff \| tree \| snapshot
2011-11-21	Andrea Asperti	Passing the right subst and metasenv when indexing...	commit \| commitdiff \| tree \| snapshot
2011-11-21	Andrea Asperti	Added a test for paramodulation filtering terms with...	commit \| commitdiff \| tree \| snapshot
2011-11-21	Andrea Asperti	More debugging info	commit \| commitdiff \| tree \| snapshot
2011-11-21	Andrea Asperti	Assert false removed (in line with the variable case).	commit \| commitdiff \| tree \| snapshot
2011-11-21	Claudio Sacerdoti...	{pattern} => in pattern;	commit \| commitdiff \| tree \| snapshot
2011-11-21	Claudio Sacerdoti...	{pattern} => in pattern;	commit \| commitdiff \| tree \| snapshot
2011-11-21	Andrea Asperti	Typo in comment	commit \| commitdiff \| tree \| snapshot
2011-11-18	Enrico Tassi	hints	commit \| commitdiff \| tree \| snapshot
2011-11-18	Enrico Tassi	coercions	commit \| commitdiff \| tree \| snapshot
2011-11-18	Wilmer Ricciotti	Solves a bug that caused the auto statistics to refer...	commit \| commitdiff \| tree \| snapshot
2011-11-18	Wilmer Ricciotti	Added help for discriminator and inverter.	commit \| commitdiff \| tree \| snapshot
2011-11-18	Enrico Tassi	short notation for "coercion"	commit \| commitdiff \| tree \| snapshot
2011-11-18	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2011-11-18	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2011-11-18	Enrico Tassi	minor Makefile fixes for the release	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom