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-23 |
Enrico Tassi | notation support fixed to parentesize in a more sane... |
tree | commitdiff |
2008-06-23 |
Enrico Tassi | xxx |
tree | commitdiff |
2008-06-22 |
Ferruccio Guidi | - grafiteParser.ml: the callback invocation was displaced |
tree | commitdiff |
2008-06-20 |
Enrico Tassi | left -> right |
tree | commitdiff |
2008-06-20 |
Claudio Sacerdoti... | Fixed bugs in the documentation of notation. |
tree | commitdiff |
2008-06-20 |
Claudio Sacerdoti... | More documentation for notation. |
tree | commitdiff |
2008-06-20 |
Claudio Sacerdoti... | Further documentation for notation. |
tree | commitdiff |
2008-06-20 |
Claudio Sacerdoti... | - partial implementation of pattern for case documented |
tree | commitdiff |
2008-06-19 |
Enrico Tassi | fixed core notation |
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-19 |
Enrico Tassi | notation on steroids: 'term 40 x' is a valid variable... |
tree | commitdiff |
2008-06-18 |
Claudio Sacerdoti... | interpretation documented |
tree | commitdiff |
2008-06-18 |
Enrico Tassi | removed unused variable |
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-17 |
Enrico Tassi | reordering of lexicon status partially avoided to make... |
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 | when -debug do not catch |
tree | commitdiff |
2008-06-13 |
Enrico Tassi | when -debug do not catch |
tree | commitdiff |
2008-06-13 |
Claudio Sacerdoti... | New lemma |
tree | commitdiff |
2008-06-13 |
Enrico Tassi | more notation |
tree | commitdiff |
2008-06-13 |
Enrico Tassi | ... |
tree | commitdiff |
2008-06-12 |
Enrico Tassi | Testing some performance tricks by caching the list... |
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 |
Claudio Sacerdoti... | New, much faster implementation of factorize. |
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-08 |
Claudio Sacerdoti... | generalize no more required before elim |
tree | commitdiff |
2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
tree | commitdiff |
2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
tree | commitdiff |
2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
tree | commitdiff |
2008-06-08 |
Claudio Sacerdoti... | generalize no more required by elim |
tree | commitdiff |
2008-06-08 |
Claudio Sacerdoti... | Generalize no more required for elim. |
tree | commitdiff |
2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
tree | commitdiff |
2008-06-08 |
Claudio Sacerdoti... | generalize no more useful for elim |
tree | commitdiff |
2008-06-08 |
Claudio Sacerdoti... | New: pattern for elim documented. |
tree | commitdiff |
2008-06-08 |
Claudio Sacerdoti... | Hypotheses patterns for elim implemented. No more need... |
tree | commitdiff |
2008-06-07 |
Enrico Tassi | exhaustivity defined |
tree | commitdiff |
2008-06-07 |
Enrico Tassi | proof simplified |
tree | commitdiff |
2008-06-06 |
Claudio Sacerdoti... | Even more Q stuff moved around. |
tree | commitdiff |
2008-06-06 |
Claudio Sacerdoti... | Even more Q stuff classified. |
tree | commitdiff |
2008-06-06 |
Enrico Tassi | lemma 3.6 subverted |
tree | commitdiff |
2008-06-06 |
Claudio Sacerdoti... | more stuff moved around |
tree | commitdiff |
2008-06-06 |
Claudio Sacerdoti... | More Q stuff organized in a coherent way. |
tree | commitdiff |
2008-06-06 |
Claudio Sacerdoti... | First snapshot at trying to clean up the Q library. |
tree | commitdiff |
2008-06-06 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2008-06-06 |
Andrea Asperti | A new theorem |
tree | commitdiff |
2008-06-06 |
Andrea Asperti | cleanup |
tree | commitdiff |
2008-06-06 |
Andrea Asperti | Cleanup. |
tree | commitdiff |
2008-06-06 |
Claudio Sacerdoti... | sieve.ma now depends only on primes.ma |
tree | commitdiff |
2008-06-06 |
Andrea Asperti | Added frac.ma |
tree | commitdiff |
2008-06-06 |
Andrea Asperti | Added Qplus_andrea.ma |
tree | commitdiff |
2008-06-06 |
Claudio Sacerdoti... | Reduce reduction tactic got rid of a long time ago. |
tree | commitdiff |
2008-06-05 |
Claudio Sacerdoti... | Eratosthene's sieve factorized out of nat/bertrand... |
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 |
Claudio Sacerdoti... | Some proofs on enumerator and denominator. |
tree | commitdiff |
2008-06-03 |
Claudio Sacerdoti... | More work on rational numbers with unique representations. |
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-03 |
Enrico Tassi | xxx |
tree | commitdiff |
2008-06-01 |
Enrico Tassi | more work on supremum |
tree | commitdiff |
2008-05-30 |
Enrico Tassi | CProp hierarchy is there! |
tree | commitdiff |
2008-05-30 |
Enrico Tassi | ... |
tree | commitdiff |
2008-05-30 |
Enrico Tassi | garbage removed |
tree | commitdiff |
2008-05-30 |
Enrico Tassi | more work on dama |
tree | commitdiff |
2008-05-30 |
Enrico Tassi | added CProp |
tree | commitdiff |
2008-05-29 |
Enrico Tassi | case not unfilding fixed |
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-29 |
Enrico Tassi | ... |
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 | ... |
tree | commitdiff |
2008-05-27 |
Enrico Tassi | CoRN moved in contribs |
tree | commitdiff |
2008-05-27 |
Enrico Tassi | auto calls cleanup\ |
tree | commitdiff |
2008-05-26 |
Enrico Tassi | better description of declarative tactics |
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 |
next |