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

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

2011-09-06	Ferruccio Guidi	- confluence of context-free reduction on terms (tpr...	commit \| commitdiff \| tree
2011-09-05	Ferruccio Guidi	- the substitution lemma is proved!	commit \| commitdiff \| tree
2011-09-02	Ferruccio Guidi	- the theory of parallel substitution of local environments...	commit \| commitdiff \| tree
2011-08-29	Ferruccio Guidi	- we shared the atomic term constructions	commit \| commitdiff \| tree
2011-08-27	Ferruccio Guidi	- the shift function is now defined and cpr_shift_fwd...	commit \| commitdiff \| tree
2011-08-25	Ferruccio Guidi	- weakening leq, we proved cpr_bind_dx	commit \| commitdiff \| tree
2011-08-24	Ferruccio Guidi	one reduction rule (tpr) was redundant	commit \| commitdiff \| tree
2011-08-23	Ferruccio Guidi	- confluence of parallel substitution (tps) closed...	commit \| commitdiff \| tree
2011-08-22	Ferruccio Guidi	we now use non-telescopic substitution in parallel...	commit \| commitdiff \| tree
2011-08-19	Ferruccio Guidi	- tentative definition of lcpr (contex-sensitive parallel...	commit \| commitdiff \| tree
2011-08-18	Ferruccio Guidi	the refactoring was not really complete	commit \| commitdiff \| tree
2011-08-18	Ferruccio Guidi	refactoring completed	commit \| commitdiff \| tree
2011-08-18	Ferruccio Guidi	- some refactoring	commit \| commitdiff \| tree
2011-08-18	Ferruccio Guidi	- matitaclean greatly improved but ...	commit \| commitdiff \| tree
2011-08-10	Ferruccio Guidi	refactoring completed!	commit \| commitdiff \| tree
2011-08-10	Ferruccio Guidi	the refactoring continues ...	commit \| commitdiff \| tree
2011-08-10	Ferruccio Guidi	the refactoring continues ...	commit \| commitdiff \| tree
2011-08-10	Ferruccio Guidi	lambda-delta must be a contrib	commit \| commitdiff \| tree
2011-08-10	Ferruccio Guidi	lambda-delta must be a contrib	commit \| commitdiff \| tree
2011-08-10	Ferruccio Guidi	some refactoring	commit \| commitdiff \| tree
2011-08-09	Ferruccio Guidi	confluence of parallel substitution (tps) started ...	commit \| commitdiff \| tree
2011-08-08	Ferruccio Guidi	- tps_tpr closed! (substitution is a reduction)	commit \| commitdiff \| tree
2011-08-07	Ferruccio Guidi	- cpr is now defined and the cpr_flat propery is proved...	commit \| commitdiff \| tree
2011-08-06	Ferruccio Guidi	- transitivity of parallel telescopic substitution...	commit \| commitdiff \| tree
2011-08-03	Ferruccio Guidi	the generation of the multiple conjunction is now supported!	commit \| commitdiff \| tree
2011-07-29	Ferruccio Guidi	confluence of tpr completed!	commit \| commitdiff \| tree
2011-07-28	Ferruccio Guidi	confluence: case 13 closed	commit \| commitdiff \| tree
2011-07-28	Ferruccio Guidi	xoa: new binary for the generation of multiple logical...	commit \| commitdiff \| tree
2011-07-27	Ferruccio Guidi	- xoa: bug fix and improvement	commit \| commitdiff \| tree
2011-07-26	Ferruccio Guidi	tpr: more inversion lemmas and a main property stated	commit \| commitdiff \| tree
2011-07-25	Ferruccio Guidi	lift_weight: bug fix	commit \| commitdiff \| tree
2011-07-25	Ferruccio Guidi	- inversion lemmas for tpr completed!	commit \| commitdiff \| tree
2011-07-24	Ferruccio Guidi	- some renaming	commit \| commitdiff \| tree
2011-07-24	Ferruccio Guidi	- sone refactoring	commit \| commitdiff \| tree
2011-07-22	Ferruccio Guidi	confluence of reduction started ...	commit \| commitdiff \| tree
2011-07-21	Ferruccio Guidi	one main propery of drop closed, one added	commit \| commitdiff \| tree
2011-07-20	Ferruccio Guidi	two more main properties of drop closed	commit \| commitdiff \| tree
2011-07-19	Ferruccio Guidi	first main property of drop closed	commit \| commitdiff \| tree
2011-07-19	Ferruccio Guidi	- drop_main: bug fix	commit \| commitdiff \| tree
2011-07-19	Ferruccio Guidi	- nnAuto.ml: width overflows are warnings, not errors	commit \| commitdiff \| tree
2011-07-19	Ferruccio Guidi	one main property of lift closed	commit \| commitdiff \| tree
2011-07-18	Ferruccio Guidi	- functional properties of lift closed!	commit \| commitdiff \| tree
2011-07-17	Ferruccio Guidi	more lemmas and some generated logical constants for...	commit \| commitdiff \| tree
2011-07-13	Ferruccio Guidi	- new definition of subst based on drop	commit \| commitdiff \| tree
2011-06-25	Ferruccio Guidi	long file names caused indentation underflow (String...	commit \| commitdiff \| tree
2011-06-25	Ferruccio Guidi	- some depend files	commit \| commitdiff \| tree
2011-06-21	Ferruccio Guidi	missing ; to delimit syntax :(	commit \| commitdiff \| tree
2011-06-18	Ferruccio Guidi	- xoa: more existential types	commit \| commitdiff \| tree
2011-06-14	Ferruccio Guidi	some restructuring	commit \| commitdiff \| tree
2011-06-14	Ferruccio Guidi	more lemmas to prove and a correction in subst	commit \| commitdiff \| tree
2011-06-13	Ferruccio Guidi	more notation and one more lemma to prove :(	commit \| commitdiff \| tree
2011-06-13	Ferruccio Guidi	reductions rules and one lemma	commit \| commitdiff \| tree
2011-06-12	Ferruccio Guidi	more properties of relocation	commit \| commitdiff \| tree
2011-06-07	Ferruccio Guidi	- we removed the reduction-related item categorization	commit \| commitdiff \| tree
2011-06-06	Ferruccio Guidi	We reintroduce the distinction between binding and...	commit \| commitdiff \| tree
2011-06-03	Ferruccio Guidi	- we introduce extended existentials (generated)	commit \| commitdiff \| tree
2011-06-03	Ferruccio Guidi	Max width overflows, which cause auto to fail, are...	commit \| commitdiff \| tree
2011-06-01	Ferruccio Guidi	CC2FO_K_cube: soundness of the K interpretation stated	commit \| commitdiff \| tree
2011-06-01	Ferruccio Guidi	subst.ma: some additions	commit \| commitdiff \| tree
2011-05-30	Ferruccio Guidi	auto does not work here :(	commit \| commitdiff \| tree
2011-05-30	Ferruccio Guidi	basics: some additions	commit \| commitdiff \| tree
2011-05-25	Ferruccio Guidi	- degree: some improvements and the Deg_append lemma	commit \| commitdiff \| tree
2011-05-24	Ferruccio Guidi	degree.ma: we defined the "degree" of a term, which...	commit \| commitdiff \| tree
2011-05-20	Ferruccio Guidi	- we weakened SAT3	commit \| commitdiff \| tree
2011-05-19	Ferruccio Guidi	cube.ma: some pts specifications of the lambda-cube	commit \| commitdiff \| tree
2011-05-14	Ferruccio Guidi	we added a property	commit \| commitdiff \| tree
2011-05-13	Ferruccio Guidi	ground: some arithmetical properties added	commit \| commitdiff \| tree
2011-04-28	Ferruccio Guidi	we uncommented R3 and R4 tu be used in lambda-delta	commit \| commitdiff \| tree
2011-04-28	Ferruccio Guidi	- weight: bugfix + weight-based eliminator axiomatized	commit \| commitdiff \| tree
2011-04-21	Ferruccio Guidi	- we added notation for the zetable and thetable items	commit \| commitdiff \| tree
2011-04-19	Ferruccio Guidi	notation bug fix	commit \| commitdiff \| tree
2011-04-19	Ferruccio Guidi	- some bug fixes	commit \| commitdiff \| tree
2011-04-19	Ferruccio Guidi	complete reformalization of lambda-delta in matita...	commit \| commitdiff \| tree
2011-04-19	Ferruccio Guidi	disambiguation of explicit interprettions with arguments...	commit \| commitdiff \| tree
2011-04-05	Ferruccio Guidi	we added an nmap from NCic.obj to NotationPt.obj (to...	commit \| commitdiff \| tree
2011-04-05	Ferruccio Guidi	we removed an extra dot from the "include" syntax	commit \| commitdiff \| tree
2011-04-04	Ferruccio Guidi	we introduced nterm for NotationPt.term	commit \| commitdiff \| tree
2011-03-30	Ferruccio Guidi	we proved that the union of two saturated sets is saturated	commit \| commitdiff \| tree
2011-03-23	Ferruccio Guidi	- terms.ma: we included 'is_dummy" and "neutral" (maybe...	commit \| commitdiff \| tree
2011-03-22	Ferruccio Guidi	the weakening lemma is not needed since it is assumed...	commit \| commitdiff \| tree
2011-03-22	Ferruccio Guidi	the thinning lemma follows immediately from the substitution...	commit \| commitdiff \| tree
2011-03-22	Ferruccio Guidi	- lambda_notation.ma: more notation and bug fixes	commit \| commitdiff \| tree
2011-03-15	Ferruccio Guidi	- more notation and service lemmas	commit \| commitdiff \| tree
2011-03-15	Ferruccio Guidi	- some ignores	commit \| commitdiff \| tree
2011-03-14	Ferruccio Guidi	dependences fix	commit \| commitdiff \| tree
2011-03-09	Ferruccio Guidi	more notation and all-purpose lemmas	commit \| commitdiff \| tree
2011-03-09	Ferruccio Guidi	the interpretation for Sigma was missing	commit \| commitdiff \| tree
2011-03-02	Ferruccio Guidi	we started the implementation of higher order saturated...	commit \| commitdiff \| tree
2011-02-27	Ferruccio Guidi	- rc_sat.ma: we changed the notation for extensional...	commit \| commitdiff \| tree
2011-02-27	Ferruccio Guidi	- notation is now in a separate file	commit \| commitdiff \| tree
2011-02-26	Ferruccio Guidi	- new file ext.ma with the objects needed for the normalizat...	commit \| commitdiff \| tree
2011-02-21	Ferruccio Guidi	we started to set up the strong normalization proof.	commit \| commitdiff \| tree
2011-02-10	Ferruccio Guidi	we added some comments	commit \| commitdiff \| tree
2011-01-02	Ferruccio Guidi	ops, we forgot to update the version indicator :)	commit \| commitdiff \| tree
2011-01-02	Ferruccio Guidi	- ld-html-root: ported to permanent lambda-delta url	commit \| commitdiff \| tree
2010-12-03	Ferruccio Guidi	first commit for Helena 0.8.2	commit \| commitdiff \| tree
2010-11-19	Ferruccio Guidi	- lddl html pages: the transition to xhtml 1.1 + css...	commit \| commitdiff \| tree
2010-11-17	Ferruccio Guidi	we updated the css validation icon	commit \| commitdiff \| tree
2010-11-17	Ferruccio Guidi	we are migrating the static htnl pagest to html 4 to...	commit \| commitdiff \| tree
2010-11-04	Ferruccio Guidi	- some changes in the crux icon	commit \| commitdiff \| tree
next

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

RSS Atom