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

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

2012-02-18	Ferruccio Guidi	more results on strongly normalizing terms	commit \| commitdiff \| tree \| snapshot
2012-02-14	Ferruccio Guidi	additions to Basic_2	commit \| commitdiff \| tree \| snapshot
2012-02-14	Ferruccio Guidi	- more properties on strongly normalizing terms	commit \| commitdiff \| tree \| snapshot
2012-02-11	Ferruccio Guidi	additions to Basic_2	commit \| commitdiff \| tree \| snapshot
2012-02-11	Ferruccio Guidi	- strong normalization of abbreviation proved	commit \| commitdiff \| tree \| snapshot
2012-02-09	Ferruccio Guidi	- design table for Basic_2	commit \| commitdiff \| tree \| snapshot
2012-02-09	Ferruccio Guidi	- first properties of strongly normalizing terms	commit \| commitdiff \| tree \| snapshot
2012-02-02	Ferruccio Guidi	- one file and three lemmas added to Basic 2	commit \| commitdiff \| tree \| snapshot
2012-02-02	Ferruccio Guidi	- three lemmas on context sensitive parallel reduction...	commit \| commitdiff \| tree \| snapshot
2012-02-01	Ferruccio Guidi	- notation fix for reducible and normal forms	commit \| commitdiff \| tree \| snapshot
2012-02-01	Ferruccio Guidi	the Basic_2 page was not regenerated ...	commit \| commitdiff \| tree \| snapshot
2012-02-01	Ferruccio Guidi	we added summary and timeline to the Basic_2 page	commit \| commitdiff \| tree \| snapshot
2012-01-31	Claudio Sacerdoti...	Notation for destructuring let-in for triples fixed.	commit \| commitdiff \| tree \| snapshot
2012-01-29	Ferruccio Guidi	- transitivity of lenv refinement for atomic arity...	commit \| commitdiff \| tree \| snapshot
2012-01-29	Ferruccio Guidi	more files added to Basic_2	commit \| commitdiff \| tree \| snapshot
2012-01-27	Ferruccio Guidi	support for abstract candidates of reducibility closed...	commit \| commitdiff \| tree \| snapshot
2012-01-27	Ferruccio Guidi	more files added to Basic_2	commit \| commitdiff \| tree \| snapshot
2012-01-27	Wilmer Ricciotti	Fixes a bug in is_flexible (when checking a meta in...	commit \| commitdiff \| tree \| snapshot
2012-01-27	Claudio Sacerdoti...	Better error messages.	commit \| commitdiff \| tree \| snapshot
2012-01-26	Ferruccio Guidi	- one file added to Basic_2	commit \| commitdiff \| tree \| snapshot
2012-01-26	Ferruccio Guidi	- main lemmas about abstract reducibility candidates...	commit \| commitdiff \| tree \| snapshot
2012-01-23	Wilmer Ricciotti	Inversion principles generation falls back to cases...	commit \| commitdiff \| tree \| snapshot
2012-01-21	Ferruccio Guidi	big fixin the structure of Basic_2	commit \| commitdiff \| tree \| snapshot
2012-01-21	Ferruccio Guidi	more files to Basic_2	commit \| commitdiff \| tree \| snapshot
2012-01-21	Ferruccio Guidi	- main proof for strong normalization closed! ...	commit \| commitdiff \| tree \| snapshot
2012-01-19	Ferruccio Guidi	closure property S4 added to abstract candidates of...	commit \| commitdiff \| tree \| snapshot
2012-01-16	Ferruccio Guidi	the support for candidates of reducibility continues ...	commit \| commitdiff \| tree \| snapshot
2012-01-16	Ferruccio Guidi	some additionsand refactoring in Basic_2	commit \| commitdiff \| tree \| snapshot
2012-01-13	Ferruccio Guidi	more file names added to Basic_2	commit \| commitdiff \| tree \| snapshot
2012-01-13	Ferruccio Guidi	- the development of abstract reducibility candidates...	commit \| commitdiff \| tree \| snapshot
2012-01-12	Wilmer Ricciotti	Improves the presentation of hypotheses in the goal...	commit \| commitdiff \| tree \| snapshot
2012-01-11	Wilmer Ricciotti	Fixes r11788 (partial, thus broken commit).	commit \| commitdiff \| tree \| snapshot
2012-01-10	Ferruccio Guidi	unpatched version for the new CamplP5	commit \| commitdiff \| tree \| snapshot
2012-01-10	Ferruccio Guidi	patched version for old CamlP5	commit \| commitdiff \| tree \| snapshot
2012-01-10	Wilmer Ricciotti	Bugfix: NCicUnification.could_reduce now performs whd...	commit \| commitdiff \| tree \| snapshot
2012-01-10	Andrea Asperti	A complete snapshot for re	commit \| commitdiff \| tree \| snapshot
2012-01-08	Ferruccio Guidi	more characters shortcuts	commit \| commitdiff \| tree \| snapshot
2012-01-08	Ferruccio Guidi	Basic_2: restyling and more notation	commit \| commitdiff \| tree \| snapshot
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
next

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

RSS Atom