| 2007-11-08 |
Enrico Tassi | ported to the new destruct |
tree | commitdiff |
| 2007-11-06 |
Ferruccio Guidi | new implementation of the destruct tactic, |
tree | commitdiff |
| 2007-10-28 |
Claudio Sacerdoti... | Nil => nil, Cons => cons |
tree | commitdiff |
| 2007-10-28 |
Claudio Sacerdoti... | Nil => nil; Cons => cons |
tree | commitdiff |
| 2007-10-28 |
Claudio Sacerdoti... | New syntax for match patterns. |
tree | commitdiff |
| 2007-10-25 |
Claudio Sacerdoti... | neg => Qneg :-) |
tree | commitdiff |
| 2007-10-25 |
Claudio Sacerdoti... | true and false were swapped! |
tree | commitdiff |
| 2007-10-25 |
Claudio Sacerdoti... | flase => false :-) |
tree | commitdiff |
| 2007-10-16 |
Claudio Sacerdoti... | Interesting. Do we need many more inversion lemmas... |
tree | commitdiff |
| 2007-10-14 |
Claudio Sacerdoti... | Caseness problems fixed. |
tree | commitdiff |
| 2007-10-14 |
Claudio Sacerdoti... | Some lemmas moves to the file they belong to. |
tree | commitdiff |
| 2007-10-14 |
Cristian Armentano | Theorem sigma_p_knm changed into generic_iter_p_knm. |
tree | commitdiff |
| 2007-10-12 |
Claudio Sacerdoti... | Move to OCaml 3.10. Requires debian packages from unsta... |
tree | commitdiff |
| 2007-10-12 |
Wilmer Ricciotti | Fixed baseuri |
tree | commitdiff |
| 2007-10-12 |
Wilmer Ricciotti | Part1a update... |
tree | commitdiff |
| 2007-10-12 |
Andrea Asperti | More restructuring in moebius.ma |
tree | commitdiff |
| 2007-10-12 |
Andrea Asperti | Reorganization of the library. |
tree | commitdiff |
| 2007-10-12 |
Andrea Asperti | Reorganization of the library. |
tree | commitdiff |
| 2007-10-12 |
Andrea Asperti | Reorganization of results. |
tree | commitdiff |
| 2007-10-08 |
Andrea Asperti | Some axioms for Q. |
tree | commitdiff |
| 2007-09-24 |
Wilmer Ricciotti | Last version of poplmark 1a, featuring new proof, only... |
tree | commitdiff |
| 2007-09-20 |
Cristian Armentano | Further simplifications to the main theorem about Euler... |
tree | commitdiff |
| 2007-09-19 |
Cristian Armentano | * Some simplifications to theorem in file totient1.ma. |
tree | commitdiff |
| 2007-09-18 |
Cristian Armentano | some theorems have been moved to more appropriate files... |
tree | commitdiff |
| 2007-09-17 |
Cristian Armentano | temporary changes, before the complete cancellation... |
tree | commitdiff |
| 2007-09-17 |
Cristian Armentano | simplified version of a theorem. |
tree | commitdiff |
| 2007-09-17 |
Andrea Asperti | Some new lemmas. |
tree | commitdiff |
| 2007-09-17 |
Andrea Asperti | A new function. |
tree | commitdiff |
| 2007-09-14 |
Andrea Asperti | Qualche semplificazione. |
tree | commitdiff |
| 2007-09-12 |
Wilmer Ricciotti | Updated, proofs are now about 750 lines. |
tree | commitdiff |
| 2007-09-11 |
Cristian Armentano | some theorem names changed. |
tree | commitdiff |
| 2007-09-10 |
Cristian Armentano | other simplifications. |
tree | commitdiff |
| 2007-09-09 |
Enrico Tassi | ... |
tree | commitdiff |
| 2007-09-09 |
Cristian Armentano | other simplifications. |
tree | commitdiff |
| 2007-09-08 |
Enrico Tassi | ... |
tree | commitdiff |
| 2007-09-07 |
Cristian Armentano | some simplifications. |
tree | commitdiff |
| 2007-09-06 |
Cristian Armentano | Some simplifications. |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | more stuff to reach an intensional definition of finite... |
tree | commitdiff |
| 2007-08-28 |
Claudio Sacerdoti... | * definition of implication free propositional formulas |
tree | commitdiff |
| 2007-08-16 |
Cristian Armentano | little change to theorem eq_gcd_times_times_eqv_times_gcd |
tree | commitdiff |
| 2007-07-31 |
Andrea Asperti | removed generic_sigma_p since generic_iter_p is the... |
tree | commitdiff |
| 2007-07-31 |
Enrico Tassi | something was really too slow... |
tree | commitdiff |
| 2007-07-30 |
Cristian Armentano | renamed generic_sigma_p.ma to generic_iter_p.ma |
tree | commitdiff |
| 2007-07-26 |
Wilmer Ricciotti | Some notation added |
tree | commitdiff |
| 2007-07-25 |
Enrico Tassi | added some notation |
tree | commitdiff |
| 2007-07-23 |
Claudio Sacerdoti... | Prototype of min_aux changed. |
tree | commitdiff |
| 2007-07-20 |
Claudio Sacerdoti... | Another nicer version. |
tree | commitdiff |
| 2007-07-20 |
Claudio Sacerdoti... | Even nicer script. |
tree | commitdiff |
| 2007-07-20 |
Claudio Sacerdoti... | The nicest script obtained so far. |
tree | commitdiff |
| 2007-07-20 |
Claudio Sacerdoti... | More simplification due to the new conversion strategy. |
tree | commitdiff |
| 2007-07-20 |
Claudio Sacerdoti... | Script simplification due to the new efficient conversi... |
tree | commitdiff |
| 2007-07-19 |
Claudio Sacerdoti... | Super-nice notation for the assembly stuff. |
tree | commitdiff |
| 2007-07-17 |
Claudio Sacerdoti... | added missing parenthesis |
tree | commitdiff |
| 2007-07-17 |
Enrico Tassi | fixed includes and added notation for bytes |
tree | commitdiff |
| 2007-07-16 |
Claudio Sacerdoti... | More lemmas. |
tree | commitdiff |
| 2007-07-16 |
Claudio Sacerdoti... | More daemons closed. A couple left in byte and many... |
tree | commitdiff |
| 2007-07-16 |
Claudio Sacerdoti... | More daemons/axioms closed. |
tree | commitdiff |
| 2007-07-16 |
Claudio Sacerdoti... | One daemon less. |
tree | commitdiff |
| 2007-07-16 |
Claudio Sacerdoti... | More daemons got rid of (and more extra axioms to be... |
tree | commitdiff |
| 2007-07-16 |
Claudio Sacerdoti... | Last daemon killed :-) |
tree | commitdiff |
| 2007-07-16 |
Claudio Sacerdoti... | One less daemon (about "update"s). |
tree | commitdiff |
| 2007-07-16 |
Claudio Sacerdoti... | All sub-proofs about "update" closed. |
tree | commitdiff |
| 2007-07-16 |
Claudio Sacerdoti... | assembly.ma splitted into many files |
tree | commitdiff |
| 2007-07-16 |
Wilmer Ricciotti | corrected axiom mod_plus |
tree | commitdiff |
| 2007-07-13 |
Claudio Sacerdoti... | More conjectures closed. |
tree | commitdiff |
| 2007-07-13 |
Claudio Sacerdoti... | 1. requires the new pretty printer for natural numbers |
tree | commitdiff |
| 2007-07-13 |
Claudio Sacerdoti... | Final theorem proved. Many many conjectures left. I... |
tree | commitdiff |
| 2007-07-12 |
Claudio Sacerdoti... | The loop invariant I chosed was not correct! |
tree | commitdiff |
| 2007-07-11 |
Claudio Sacerdoti... | Getting close to the final result. |
tree | commitdiff |
| 2007-07-11 |
Claudio Sacerdoti... | 1. loop invariant stated, but not proved |
tree | commitdiff |
| 2007-07-11 |
Claudio Sacerdoti... | 1. status factorized out in tick |
tree | commitdiff |
| 2007-07-10 |
Claudio Sacerdoti... | 0. less nice solution by Enrico reverted |
tree | commitdiff |
| 2007-07-10 |
Enrico Tassi | La programmazione funzionale e' come TeX, funziona... |
tree | commitdiff |
| 2007-07-09 |
Enrico Tassi | 1. bug fixed in tick |
tree | commitdiff |
| 2007-07-09 |
Claudio Sacerdoti... | Interesting theorem added (but still to be proved). |
tree | commitdiff |
| 2007-07-07 |
Enrico Tassi | inclusion of div_and_mod |
tree | commitdiff |
| 2007-07-06 |
Enrico Tassi | maxipatch for support of multiple DBs. |
tree | commitdiff |
| 2007-07-05 |
Claudio Sacerdoti... | Exadecimal numbers are now used. This is a great speed-up. |
tree | commitdiff |
| 2007-07-04 |
Claudio Sacerdoti... | Example program executed for x,y=0. |
tree | commitdiff |
| 2007-07-04 |
Claudio Sacerdoti... | Quick hack: matita natural numbers are now accepted... |
tree | commitdiff |
| 2007-07-04 |
Claudio Sacerdoti... | More opcodes (badly) implemented. |
tree | commitdiff |
| 2007-07-04 |
Claudio Sacerdoti... | List.ma: added function nth (with default value in... |
tree | commitdiff |
| 2007-06-30 |
Cristian Armentano | New definition of Euler's totient function. |
tree | commitdiff |
| 2007-06-29 |
Cristian Armentano | generic version, specializing generic_sigma_p.ma |
tree | commitdiff |
| 2007-06-29 |
Cristian Armentano | generic version |
tree | commitdiff |
| 2007-06-29 |
Cristian Armentano | theorems about sigma_p proved using sigma_p_gen |
tree | commitdiff |
| 2007-06-27 |
Cristian Armentano | new gcd properties, and theorems for totient, and theor... |
tree | commitdiff |
| 2007-06-26 |
Cristian Armentano | (no commit message) |
tree | commitdiff |
| 2007-06-26 |
Cristian Armentano | generic sommatory. |
tree | commitdiff |
| 2007-06-21 |
Wilmer Ricciotti | PoplMark challenge part 1a: new, shorter version w... |
tree | commitdiff |
| 2007-05-24 |
Enrico Tassi | auto and autogui... some work |
tree | commitdiff |
| 2007-05-20 |
Ferruccio Guidi | applyTransformation: added debugging information |
tree | commitdiff |
| 2007-05-17 |
Enrico Tassi | auto rewritten with only one tail recursive function. |
tree | commitdiff |
| 2007-05-09 |
Andrea Asperti | A few extensions for the moebius inversion theorem |
tree | commitdiff |
| 2007-05-09 |
Andrea Asperti | Proof of the moebius inversion theorem |
tree | commitdiff |
| 2007-04-20 |
Claudio Sacerdoti... | Much ado about nothing: |
tree | commitdiff |
| 2007-04-18 |
Enrico Tassi | more discriminate |
tree | commitdiff |
| 2007-04-16 |
Enrico Tassi | better simplify |
tree | commitdiff |
| 2007-04-16 |
Enrico Tassi | closed all axioms |
tree | commitdiff |
| 2007-04-10 |
Enrico Tassi | set -> type |
tree | commitdiff |
| next |
projects / helm.git / history