| 2008-06-26 |
Enrico Tassi | some more work |
tree | commitdiff |
| 2008-06-26 |
Enrico Tassi | more work on q |
tree | commitdiff |
| 2008-06-25 |
Enrico Tassi | some more work |
tree | commitdiff |
| 2008-06-25 |
Enrico Tassi | better, reparsable, notation |
tree | commitdiff |
| 2008-06-24 |
Enrico Tassi | removed <_,_> notation second interpretation for depend... |
tree | commitdiff |
| 2008-06-24 |
Enrico Tassi | notation factored, coercion commant taking terms and... |
tree | commitdiff |
| 2008-06-23 |
Enrico Tassi | more work, but russell too slow |
tree | commitdiff |
| 2008-06-22 |
Ferruccio Guidi | - grafiteParser.ml: the callback invocation was displaced |
tree | commitdiff |
| 2008-06-19 |
Claudio Sacerdoti... | - notation fixed according to the new stricter semantics |
tree | commitdiff |
| 2008-06-19 |
Ferruccio Guidi | - Procedural: we now check that an eliminator opens... |
tree | commitdiff |
| 2008-06-18 |
Enrico Tassi | some work on Q |
tree | commitdiff |
| 2008-06-17 |
Enrico Tassi | general reorganization and first (unconditional) proof... |
tree | commitdiff |
| 2008-06-16 |
Enrico Tassi | Dedekind sigma completeness for the natural numbers. |
tree | commitdiff |
| 2008-06-16 |
Enrico Tassi | typo |
tree | commitdiff |
| 2008-06-13 |
Enrico Tassi | some notation added with a bit PITA |
tree | commitdiff |
| 2008-06-13 |
Enrico Tassi | more notation |
tree | commitdiff |
| 2008-06-12 |
Enrico Tassi | better names in a lemma to increase readability |
tree | commitdiff |
| 2008-06-12 |
Enrico Tassi | fixed some regressions |
tree | commitdiff |
| 2008-06-11 |
Enrico Tassi | gran casino |
tree | commitdiff |
| 2008-06-10 |
Enrico Tassi | bla bla bla |
tree | commitdiff |
| 2008-06-10 |
Enrico Tassi | initial qork for models |
tree | commitdiff |
| 2008-06-10 |
Enrico Tassi | lebesgue proved |
tree | commitdiff |
| 2008-06-10 |
Enrico Tassi | snapshot |
tree | commitdiff |
| 2008-06-09 |
Claudio Sacerdoti... | Most of the time, URIs can now be replaced with identif... |
tree | commitdiff |
| 2008-06-09 |
Enrico Tassi | initial work on lebesque |
tree | commitdiff |
| 2008-06-09 |
Enrico Tassi | exhaustivity completed |
tree | commitdiff |
| 2008-06-09 |
Enrico Tassi | exhaustivity, some work |
tree | commitdiff |
| 2008-06-07 |
Enrico Tassi | exhaustivity defined |
tree | commitdiff |
| 2008-06-07 |
Enrico Tassi | proof simplified |
tree | commitdiff |
| 2008-06-06 |
Enrico Tassi | lemma 3.6 subverted |
tree | commitdiff |
| 2008-06-05 |
Enrico Tassi | .... |
tree | commitdiff |
| 2008-06-05 |
Enrico Tassi | added order_continuity |
tree | commitdiff |
| 2008-06-05 |
Enrico Tassi | sandwich is back |
tree | commitdiff |
| 2008-06-03 |
Enrico Tassi | some work on uniformity |
tree | commitdiff |
| 2008-06-03 |
Enrico Tassi | end of section 2.2 |
tree | commitdiff |
| 2008-06-03 |
Enrico Tassi | proof refactored |
tree | commitdiff |
| 2008-06-01 |
Enrico Tassi | more work on supremum |
tree | commitdiff |
| 2008-05-30 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-05-30 |
Enrico Tassi | more work on dama |
tree | commitdiff |
| 2008-05-29 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-05-29 |
Enrico Tassi | first page of the new dama proof |
tree | commitdiff |
| 2008-05-28 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-05-28 |
Enrico Tassi | dama restarted |
tree | commitdiff |
| 2008-05-28 |
Enrico Tassi | cleanup |
tree | commitdiff |
| 2008-05-28 |
Enrico Tassi | the attempt of completing dama using duality frozen |
tree | commitdiff |
| 2008-05-27 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-05-27 |
Enrico Tassi | smarter lexer needed by lambda-delta that is splitting... |
tree | commitdiff |
| 2008-05-27 |
Enrico Tassi | CoRN moved in contribs |
tree | commitdiff |
| 2008-05-26 |
Enrico Tassi | new, more rigid syntax, for auto_params affecting the... |
tree | commitdiff |
| 2008-05-26 |
Ferruccio Guidi | - some bugs fixed in the domain-based preorders on... |
tree | commitdiff |
| 2008-05-19 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Enrico Tassi | run fsub during night |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Enrico Tassi | names fixed accoding to the new ones generated after... |
tree | commitdiff |
| 2008-05-02 |
Wilmer Ricciotti | Some destruct tactics got broken after last update... |
tree | commitdiff |
| 2008-04-24 |
Wilmer Ricciotti | Proof of adequacy. |
tree | commitdiff |
| 2008-04-21 |
Claudio Sacerdoti... | defn2.ma is to be used with part1a_inversion3 |
tree | commitdiff |
| 2008-04-20 |
Claudio Sacerdoti... | Alternative prove using just one induction/inversion... |
tree | commitdiff |
| 2008-04-18 |
Claudio Sacerdoti... | Dead code removed. |
tree | commitdiff |
| 2008-04-18 |
Claudio Sacerdoti... | Inversion lemma for Forall. |
tree | commitdiff |
| 2008-04-11 |
Claudio Sacerdoti... | Extracted code. The main executable is medium_tests... |
tree | commitdiff |
| 2008-03-26 |
Wilmer Ricciotti | Reorganization of list library (step 1) |
tree | commitdiff |
| 2008-03-25 |
Enrico Tassi | fix with m (to be optimized) are rewritten such that... |
tree | commitdiff |
| 2008-03-25 |
Enrico Tassi | very very interesting hack |
tree | commitdiff |
| 2008-03-25 |
Enrico Tassi | argument of type mcu_type always abstracted first |
tree | commitdiff |
| 2008-03-23 |
Enrico Tassi | Fsub moved in contribs |
tree | commitdiff |
| 2008-03-23 |
Ferruccio Guidi | cicNotationPp: fixed letin syntax (now typeless) |
tree | commitdiff |
| 2008-03-22 |
Enrico Tassi | library_auto moved inside contrib, still not ported... |
tree | commitdiff |
| 2008-03-22 |
Enrico Tassi | moved dama/ and dama_didactic/ in contribs/dama/ |
tree | commitdiff |
| 2008-03-22 |
Enrico Tassi | freescale moved under contribs. contribs made relocatable |
tree | commitdiff |
| 2008-03-20 |
Ferruccio Guidi | Base-2 is not compiling properly and is excluded for now |
tree | commitdiff |
| 2008-03-19 |
Ferruccio Guidi | Procedural : added some missing cases |
tree | commitdiff |
| 2008-03-18 |
Ferruccio Guidi | LAMBDA-TYPES: level 2 dependences are now correct,... |
tree | commitdiff |
| 2008-03-18 |
Ferruccio Guidi | Procedural : tentative update to the new letin cic... |
tree | commitdiff |
| 2008-03-09 |
Ferruccio Guidi | LAMBDA-TYPES: some more generation lemmas and some... |
tree | commitdiff |
| 2008-03-05 |
Ferruccio Guidi | some corrections and additions |
tree | commitdiff |
| 2008-03-04 |
Ferruccio Guidi | components/library: dotdothack removed |
tree | commitdiff |
| 2008-02-29 |
Ferruccio Guidi | we added the classic substitution function |
tree | commitdiff |
| 2008-02-26 |
Ferruccio Guidi | LAMBDA-TYPES: added wf3 (legal context predicate); |
tree | commitdiff |
| 2008-02-24 |
Ferruccio Guidi | $(H) added :) |
tree | commitdiff |
| 2008-02-24 |
Ferruccio Guidi | LAMBDA-TYPES: dependences calculation improved |
tree | commitdiff |
| 2008-02-23 |
Ferruccio Guidi | LAMBDA-TYPES: |
tree | commitdiff |
| 2008-02-22 |
Ferruccio Guidi | - added some options to matitadep: -stdout and -exclude |
tree | commitdiff |
| 2008-02-21 |
Ferruccio Guidi | svn:ignores fixed |
tree | commitdiff |
| 2008-02-20 |
Ferruccio Guidi | -onepass option removed from Makefile to comile Base... |
tree | commitdiff |
| 2008-02-20 |
Ferruccio Guidi | LambdaDelta-1 regenerated as a subdevel ov LAMBDA-TYPES |
tree | commitdiff |
| 2008-02-19 |
Ferruccio Guidi | dependences needed a fix :) |
tree | commitdiff |
| 2008-02-19 |
Ferruccio Guidi | we are moving the devel root one dir level up |
tree | commitdiff |
| 2008-02-13 |
Ferruccio Guidi | baseuris removed from files |
tree | commitdiff |
| 2008-02-13 |
Ferruccio Guidi | fixed dependences |
tree | commitdiff |
| 2008-02-13 |
Ferruccio Guidi | renaming |
tree | commitdiff |
| 2008-02-13 |
Ferruccio Guidi | renaming |
tree | commitdiff |
| 2008-02-12 |
Ferruccio Guidi | renaming |
tree | commitdiff |
| 2008-02-12 |
Ferruccio Guidi | regeneration with new results |
tree | commitdiff |
| 2008-02-12 |
Enrico Tassi | fixed path for matitadep |
tree | commitdiff |
| 2008-01-10 |
Enrico Tassi | BIG FAT WARNING: DEVELOPMENTS DIE HERE |
tree | commitdiff |
| 2007-11-12 |
Ferruccio Guidi | - destruct tactic: automatic simplification in case... |
tree | commitdiff |
| 2007-11-12 |
Ferruccio Guidi | refactoring |
tree | commitdiff |
| next |
projects / helm.git / history