| 2016-01-13 |
Ferruccio Guidi | - ng_kernel: catched Invalid_argument "List.nth" in... |
tree | commitdiff |
| 2015-10-29 |
Ferruccio Guidi | - matita: computed auto traces now include the "width... |
tree | commitdiff |
| 2015-10-25 |
Ferruccio Guidi | theory of relocation updated ..... |
tree | commitdiff |
| 2015-10-25 |
Ferruccio Guidi | theory of generic slicing almost completed .... |
tree | commitdiff |
| 2015-10-21 |
Ferruccio Guidi | parked material ... |
tree | commitdiff |
| 2015-10-21 |
Ferruccio Guidi | new results on multiple relocation |
tree | commitdiff |
| 2015-10-21 |
Ferruccio Guidi | theory of multiple relocation completed |
tree | commitdiff |
| 2015-10-21 |
Ferruccio Guidi | minor update |
tree | commitdiff |
| 2015-10-14 |
Ferruccio Guidi | colength and identity relocation |
tree | commitdiff |
| 2015-10-11 |
Ferruccio Guidi | ground_2: added missing file |
tree | commitdiff |
| 2015-10-11 |
Ferruccio Guidi | ground_2 milestone: multiple relocation with lists... |
tree | commitdiff |
| 2015-09-20 |
Ferruccio Guidi | limits: we set up a different foundation |
tree | commitdiff |
| 2015-09-06 |
Ferruccio Guidi | flavour and source information exported for the objects... |
tree | commitdiff |
| 2015-07-14 |
Ferruccio Guidi | - subtraction (and related notions) removed |
tree | commitdiff |
| 2015-03-25 |
Ferruccio Guidi | - revision of ground_2 and basic_2 |
tree | commitdiff |
| 2015-03-07 |
Ferruccio Guidi | performance data for basic_1 on dev.helm |
tree | commitdiff |
| 2015-03-06 |
Ferruccio Guidi | with matita 0.99.2 we can validate lambdadelta_1 (as... |
tree | commitdiff |
| 2015-03-06 |
Ferruccio Guidi | legacy_1, ground_1, and basic_1 recommitted without... |
tree | commitdiff |
| 2015-03-05 |
Ferruccio Guidi | basic_1: COMMIT COMPLETED |
tree | commitdiff |
| 2015-03-05 |
Ferruccio Guidi | components: pc1, pc3, ty3, csubt, ex1 |
tree | commitdiff |
| 2015-03-05 |
Ferruccio Guidi | components: sc3, csubc |
tree | commitdiff |
| 2015-03-04 |
Ferruccio Guidi | components: nf2, sn3, ex2 |
tree | commitdiff |
| 2015-03-04 |
Ferruccio Guidi | components: arity, csuba |
tree | commitdiff |
| 2015-02-25 |
Ferruccio Guidi | component: pr3 |
tree | commitdiff |
| 2015-02-24 |
Ferruccio Guidi | components: wcpr0 pr1 pr2 |
tree | commitdiff |
| 2015-02-23 |
Ferruccio Guidi | component: pr0 |
tree | commitdiff |
| 2015-02-22 |
Ferruccio Guidi | components: A asucc aplus leq llt aprem ex0 |
tree | commitdiff |
| 2015-02-19 |
Ferruccio Guidi | components: G, next_plus, sty0, sty1 |
tree | commitdiff |
| 2015-02-11 |
Ferruccio Guidi | components: subst1 csubst0 csubst1 fsubst0 |
tree | commitdiff |
| 2015-02-11 |
Ferruccio Guidi | components: subst csubv |
tree | commitdiff |
| 2015-02-10 |
Ferruccio Guidi | components: subst0 |
tree | commitdiff |
| 2015-02-09 |
Ferruccio Guidi | components: clen lift1 drop1 |
tree | commitdiff |
| 2015-02-08 |
Ferruccio Guidi | components: clear getl cimp |
tree | commitdiff |
| 2015-02-08 |
Ferruccio Guidi | components cnt drop |
tree | commitdiff |
| 2015-02-06 |
Ferruccio Guidi | some improvements in the anticipator |
tree | commitdiff |
| 2015-02-04 |
Ferruccio Guidi | components C r flt app lift |
tree | commitdiff |
| 2015-02-04 |
Ferruccio Guidi | - matitac: now directories are allowed as command line... |
tree | commitdiff |
| 2015-02-04 |
Ferruccio Guidi | - some improvements in the generation of terms |
tree | commitdiff |
| 2015-02-03 |
Ferruccio Guidi | - we generate the terms in anticipated form (the are... |
tree | commitdiff |
| 2015-01-30 |
Ferruccio Guidi | porting of basic_1 for the ng_kernel: first step ... |
tree | commitdiff |
| 2015-01-22 |
Ferruccio Guidi | refactoring of \lambda\delta version 1 in matita |
tree | commitdiff |
| 2015-01-22 |
Ferruccio Guidi | informational page on ground_1 |
tree | commitdiff |
| 2015-01-18 |
Ferruccio Guidi | - we add an informational page on \lambda\delta version... |
tree | commitdiff |
| 2014-10-28 |
Ferruccio Guidi | \lambda\delta version 2A released on Web site |
tree | commitdiff |
| 2014-10-27 |
Ferruccio Guidi | - the trace is explicit in all auto tactics with depth > 1 |
tree | commitdiff |
| 2014-10-26 |
Ferruccio Guidi | - some renaming according to the written version of... |
tree | commitdiff |
| 2014-10-19 |
Ferruccio Guidi | - grafiteParser: we added the comand "defined" as a... |
tree | commitdiff |
| 2014-10-15 |
Ferruccio Guidi | more automation for cpcs ... |
tree | commitdiff |
| 2014-10-13 |
Ferruccio Guidi | - lambdadelta: minor corrections |
tree | commitdiff |
| 2014-10-08 |
Ferruccio Guidi | - some consequences of preservation added |
tree | commitdiff |
| 2014-10-05 |
Ferruccio Guidi | catched typecheker failures in auto allow more applicat... |
tree | commitdiff |
| 2014-10-04 |
Ferruccio Guidi | the commit was incomplete (as is often the case :( ) |
tree | commitdiff |
| 2014-10-04 |
Ferruccio Guidi | - nnAuto: we catch TypeCheckerFailure generated at... |
tree | commitdiff |
| 2014-10-02 |
Ferruccio Guidi | previous commit was not complete :( |
tree | commitdiff |
| 2014-10-02 |
Ferruccio Guidi | - fpbg can be reflexive (example given) |
tree | commitdiff |
| 2014-09-30 |
Ferruccio Guidi | notation update for pointwise union |
tree | commitdiff |
| 2014-09-15 |
Ferruccio Guidi | notational change of lift, drop, and gget |
tree | commitdiff |
| 2014-09-14 |
Ferruccio Guidi | slight refactoring in the proof of strong normalization |
tree | commitdiff |
| 2014-09-12 |
Ferruccio Guidi | one more typo ... |
tree | commitdiff |
| 2014-09-12 |
Ferruccio Guidi | bug fix in ththe notation for lists: |
tree | commitdiff |
| 2014-09-10 |
Ferruccio Guidi | added an example on lstas showing a difference with... |
tree | commitdiff |
| 2014-09-10 |
Ferruccio Guidi | commit completed! the new iterated static type assignme... |
tree | commitdiff |
| 2014-09-03 |
Ferruccio Guidi | - the PARTIAL COMMIT continues, we issue the "reduction... |
tree | commitdiff |
| 2014-08-31 |
Ferruccio Guidi | - new stand-alone definition of lstas (sta and old... |
tree | commitdiff |
| 2014-08-10 |
Ferruccio Guidi | some renaming and a minor addition |
tree | commitdiff |
| 2014-08-07 |
Ferruccio Guidi | - bugfixed "aacr" allows to remove historical eta-conve... |
tree | commitdiff |
| 2014-08-06 |
Ferruccio Guidi | - some renaming and minor updates |
tree | commitdiff |
| 2014-08-05 |
Ferruccio Guidi | bugfix in source table :( |
tree | commitdiff |
| 2014-08-05 |
Ferruccio Guidi | - basic_2: reaxiomatized snv with improved cpds and... |
tree | commitdiff |
| 2014-07-31 |
Ferruccio Guidi | one property of abstract computation removed |
tree | commitdiff |
| 2014-07-18 |
Ferruccio Guidi | - irreflexivity of static type assignment iterated... |
tree | commitdiff |
| 2014-07-14 |
Ferruccio Guidi | some renaming and some typos corrected ... |
tree | commitdiff |
| 2014-07-05 |
Ferruccio Guidi | improved example: Delta must be a family of terms |
tree | commitdiff |
| 2014-07-04 |
Ferruccio Guidi | conjecture on antisymmetry of cpr finally closed |
tree | commitdiff |
| 2014-06-30 |
Ferruccio Guidi | some additions and corrections ... |
tree | commitdiff |
| 2014-06-29 |
Ferruccio Guidi | - wrong version of drop was used in four places |
tree | commitdiff |
| 2014-06-28 |
Ferruccio Guidi | - ldrop is now drop as in basic_1 |
tree | commitdiff |
| 2014-06-19 |
Ferruccio Guidi | - some pending conjectures closed in basic_2 and ground_2 |
tree | commitdiff |
| 2014-06-18 |
Ferruccio Guidi | milestone connit for preservation: |
tree | commitdiff |
| 2014-06-15 |
Ferruccio Guidi | - we introduce stratified term equivalence to remove... |
tree | commitdiff |
| 2014-06-14 |
Ferruccio Guidi | reorganization of the "static" component: |
tree | commitdiff |
| 2014-06-10 |
Ferruccio Guidi | preservation of stratified vaildity through ordinary... |
tree | commitdiff |
| 2014-06-09 |
Ferruccio Guidi | advances on append allow to complete the long awaited... |
tree | commitdiff |
| 2014-06-08 |
Ferruccio Guidi | now we use the version of lazy union for local environm... |
tree | commitdiff |
| 2014-06-08 |
Ferruccio Guidi | bug fix in lazy union for local environments |
tree | commitdiff |
| 2014-06-08 |
Ferruccio Guidi | - some work on append |
tree | commitdiff |
| 2014-06-07 |
Ferruccio Guidi | source table bugfixed |
tree | commitdiff |
| 2014-06-07 |
Ferruccio Guidi | - advances on free variables allow to reduce lleq_lpx_t... |
tree | commitdiff |
| 2014-06-01 |
Ferruccio Guidi | - some refactoring and minor additions |
tree | commitdiff |
| 2014-06-01 |
Ferruccio Guidi | - advances on hereditarily free variables: now "frees... |
tree | commitdiff |
| 2014-05-26 |
Ferruccio Guidi | one file was missing :( |
tree | commitdiff |
| 2014-05-26 |
Ferruccio Guidi | new definition of llor gives a long awaited lemma :), |
tree | commitdiff |
| 2014-05-25 |
Ferruccio Guidi | - theory of llor now includes (long awaited) non-recurs... |
tree | commitdiff |
| 2014-05-24 |
Ferruccio Guidi | non-recursive alternative of llpx_sn completed ! |
tree | commitdiff |
| 2014-05-23 |
Ferruccio Guidi | advances on cofrees allows to prove one direction of |
tree | commitdiff |
| 2014-05-11 |
Ferruccio Guidi | advances on ldrop .... |
tree | commitdiff |
| 2014-05-10 |
Ferruccio Guidi | advances on cofrees |
tree | commitdiff |
| 2014-04-27 |
Ferruccio Guidi | reordering abstract computation properties and saturati... |
tree | commitdiff |
| 2014-04-25 |
Ferruccio Guidi | one file was missing ... |
tree | commitdiff |
| 2014-04-25 |
Ferruccio Guidi | - advances in the theory of cofrees |
tree | commitdiff |
| next |
projects / helm.git / history