| 2007-07-16 | 
Claudio Sacerdoti...  | More daemons got rid of (and more extra axioms to be...  | 
commit | commitdiff | tree | snapshot | 
| 2007-07-16 | 
Claudio Sacerdoti...  | Last daemon killed :-) | 
commit | commitdiff | tree | snapshot | 
| 2007-07-16 | 
Claudio Sacerdoti...  | One less daemon (about "update"s). | 
commit | commitdiff | tree | snapshot | 
| 2007-07-16 | 
Claudio Sacerdoti...  | All sub-proofs about "update" closed. | 
commit | commitdiff | tree | snapshot | 
| 2007-07-16 | 
Claudio Sacerdoti...  | assembly.ma splitted into many files | 
commit | commitdiff | tree | snapshot | 
| 2007-07-16 | 
Stefano Zacchiroli | * NOT RELEASED YET | 
commit | commitdiff | tree | snapshot | 
| 2007-07-16 | 
Stefano Zacchiroli | * NOT RELEASED YET | 
commit | commitdiff | tree | snapshot | 
| 2007-07-16 | 
Stefano Zacchiroli | proper path for ps.gz doc | 
commit | commitdiff | tree | snapshot | 
| 2007-07-16 | 
Stefano Zacchiroli |     texlive-base-bin, texlive-latex-extra | 
commit | commitdiff | tree | snapshot | 
| 2007-07-16 | 
Stefano Zacchiroli |   - add build-dep for doc generation: graphviz, texlive...  | 
commit | commitdiff | tree | snapshot | 
| 2007-07-16 | 
Stefano Zacchiroli |   - add build-dep for doc generation: graphviz, texlive...  | 
commit | commitdiff | tree | snapshot | 
| 2007-07-16 | 
Stefano Zacchiroli | * debian/rules | 
commit | commitdiff | tree | snapshot | 
| 2007-07-16 | 
Stefano Zacchiroli | invoke make doc after build to create ocamldoc docs | 
commit | commitdiff | tree | snapshot | 
| 2007-07-16 | 
Stefano Zacchiroli | * debian/svn-deblayout | 
commit | commitdiff | tree | snapshot | 
| 2007-07-16 | 
Stefano Zacchiroli | * rebuild against OCaml 3.10 and ocamlnet 2.2 | 
commit | commitdiff | tree | snapshot | 
| 2007-07-16 | 
Stefano Zacchiroli | * debian/*.install.in | 
commit | commitdiff | tree | snapshot | 
| 2007-07-16 | 
Stefano Zacchiroli | * rebuild with OCaml 3.10 | 
commit | commitdiff | tree | snapshot | 
| 2007-07-16 | 
Wilmer Ricciotti | corrected axiom mod_plus | 
commit | commitdiff | tree | snapshot | 
| 2007-07-14 | 
Ferruccio Guidi | new definitions and new theorems | 
commit | commitdiff | tree | snapshot | 
| 2007-07-13 | 
Claudio Sacerdoti...  | More conjectures closed. | 
commit | commitdiff | tree | snapshot | 
| 2007-07-13 | 
Claudio Sacerdoti...  | 1. requires the new pretty printer for natural numbers | 
commit | commitdiff | tree | snapshot | 
| 2007-07-13 | 
Claudio Sacerdoti...  | Dirty patch by Zack: natural numbers of Matita are...  | 
commit | commitdiff | tree | snapshot | 
| 2007-07-13 | 
Claudio Sacerdoti...  | Last crazy commit reverted. | 
commit | commitdiff | tree | snapshot | 
| 2007-07-13 | 
Claudio Sacerdoti...  | Final theorem proved. Many many conjectures left. I...  | 
commit | commitdiff | tree | snapshot | 
| 2007-07-12 | 
Claudio Sacerdoti...  | The loop invariant I chosed was not correct! | 
commit | commitdiff | tree | snapshot | 
| 2007-07-11 | 
Claudio Sacerdoti...  | Getting close to the final result. | 
commit | commitdiff | tree | snapshot | 
| 2007-07-11 | 
Claudio Sacerdoti...  | 1. loop invariant stated, but not proved | 
commit | commitdiff | tree | snapshot | 
| 2007-07-11 | 
Ferruccio Guidi | native dependences fixed | 
commit | commitdiff | tree | snapshot | 
| 2007-07-11 | 
Claudio Sacerdoti...  | 1. status factorized out in tick | 
commit | commitdiff | tree | snapshot | 
| 2007-07-11 | 
Claudio Sacerdoti...  | auto new => autobatch | 
commit | commitdiff | tree | snapshot | 
| 2007-07-11 | 
Claudio Sacerdoti...  | auto new => autobatch | 
commit | commitdiff | tree | snapshot | 
| 2007-07-10 | 
Claudio Sacerdoti...  | 0. less nice solution by Enrico reverted | 
commit | commitdiff | tree | snapshot | 
| 2007-07-10 | 
Claudio Sacerdoti...  | New reduction strategy: the new reduction strategy...  | 
commit | commitdiff | tree | snapshot | 
| 2007-07-10 | 
Enrico Tassi | La programmazione funzionale e' come TeX, funziona...  | 
commit | commitdiff | tree | snapshot | 
| 2007-07-10 | 
Ferruccio Guidi | persistent inner types are now generated in publishing...  | 
commit | commitdiff | tree | snapshot | 
| 2007-07-10 | 
Enrico Tassi | fixed a bug in the cleanup ofsedir that was not properl...  | 
commit | commitdiff | tree | snapshot | 
| 2007-07-10 | 
Enrico Tassi | ... | 
commit | commitdiff | tree | snapshot | 
| 2007-07-09 | 
Enrico Tassi | 1. bug fixed in tick | 
commit | commitdiff | tree | snapshot | 
| 2007-07-09 | 
Enrico Tassi | signal hadler restored after runnig external 'make' | 
commit | commitdiff | tree | snapshot | 
| 2007-07-09 | 
Claudio Sacerdoti...  | Interesting theorem added (but still to be proved). | 
commit | commitdiff | tree | snapshot | 
| 2007-07-09 | 
Enrico Tassi | added few more fun to this test | 
commit | commitdiff | tree | snapshot | 
| 2007-07-09 | 
Ferruccio Guidi | new configuration file sample | 
commit | commitdiff | tree | snapshot | 
| 2007-07-09 | 
Ferruccio Guidi | tassi: ported to the new DB architecture. | 
commit | commitdiff | tree | snapshot | 
| 2007-07-09 | 
Enrico Tassi | auto->autobatch | 
commit | commitdiff | tree | snapshot | 
| 2007-07-07 | 
Enrico Tassi | inclusion of div_and_mod | 
commit | commitdiff | tree | snapshot | 
| 2007-07-06 | 
Enrico Tassi | maxipatch for support of multiple DBs. | 
commit | commitdiff | tree | snapshot | 
| 2007-07-05 | 
Claudio Sacerdoti...  | Exadecimal numbers are now used. This is a great speed-up. | 
commit | commitdiff | tree | snapshot | 
| 2007-07-04 | 
Claudio Sacerdoti...  | Example program executed for x,y=0. | 
commit | commitdiff | tree | snapshot | 
| 2007-07-04 | 
Claudio Sacerdoti...  | Quick hack: matita natural numbers are now accepted...  | 
commit | commitdiff | tree | snapshot | 
| 2007-07-04 | 
Claudio Sacerdoti...  | Bug fixed: a ~with_cast is now inserted when appropriat...  | 
commit | commitdiff | tree | snapshot | 
| 2007-07-04 | 
Claudio Sacerdoti...  | In place of conclude, obtain FIXMEXXX is now generated...  | 
commit | commitdiff | tree | snapshot | 
| 2007-07-04 | 
Claudio Sacerdoti...  | 1. Code simplification | 
commit | commitdiff | tree | snapshot | 
| 2007-07-04 | 
Claudio Sacerdoti...  | is_top_down was not propageted correctly under a bottom...  | 
commit | commitdiff | tree | snapshot | 
| 2007-07-04 | 
Claudio Sacerdoti...  | 1. "by proof" now allowed as a justification in equalit...  | 
commit | commitdiff | tree | snapshot | 
| 2007-07-04 | 
Claudio Sacerdoti...  | Added ~with_cast to the change tactic. | 
commit | commitdiff | tree | snapshot | 
| 2007-07-04 | 
Claudio Sacerdoti...  | Bug fixed: name in letin was printed as "previous"...  | 
commit | commitdiff | tree | snapshot | 
| 2007-07-04 | 
Claudio Sacerdoti...  | More opcodes (badly) implemented. | 
commit | commitdiff | tree | snapshot | 
| 2007-07-04 | 
Claudio Sacerdoti...  | List.ma: added function nth (with default value in...  | 
commit | commitdiff | tree | snapshot | 
| 2007-06-30 | 
Cristian Armentano | New definition of Euler's totient function. | 
commit | commitdiff | tree | snapshot | 
| 2007-06-30 | 
Claudio Sacerdoti...  | In order to generate executable declarative scripts...  | 
commit | commitdiff | tree | snapshot | 
| 2007-06-30 | 
Claudio Sacerdoti...  | Bug fixed in bottom-up conversion. | 
commit | commitdiff | tree | snapshot | 
| 2007-06-30 | 
Claudio Sacerdoti...  | BU Conversion was not generated for Rels fixed. I wonde...  | 
commit | commitdiff | tree | snapshot | 
| 2007-06-30 | 
Claudio Sacerdoti...  | Nicer layout but possibly more bugged. | 
commit | commitdiff | tree | snapshot | 
| 2007-06-30 | 
Claudio Sacerdoti...  | Spurious "we need to prove" at the beginning of Intros...  | 
commit | commitdiff | tree | snapshot | 
| 2007-06-29 | 
Cristian Armentano | generic version, specializing generic_sigma_p.ma | 
commit | commitdiff | tree | snapshot | 
| 2007-06-29 | 
Cristian Armentano | generic version | 
commit | commitdiff | tree | snapshot | 
| 2007-06-29 | 
Cristian Armentano | theorems about sigma_p proved using sigma_p_gen | 
commit | commitdiff | tree | snapshot | 
| 2007-06-27 | 
Ferruccio Guidi | svn:ignore property set | 
commit | commitdiff | tree | snapshot | 
| 2007-06-27 | 
Cristian Armentano | new gcd properties, and theorems for totient, and theor...  | 
commit | commitdiff | tree | snapshot | 
| 2007-06-26 | 
Ferruccio Guidi | some old auto yurned into autobatch | 
commit | commitdiff | tree | snapshot | 
| 2007-06-26 | 
Cristian Armentano | (no commit message) | 
commit | commitdiff | tree | snapshot | 
| 2007-06-26 | 
Cristian Armentano | generic sommatory. | 
commit | commitdiff | tree | snapshot | 
| 2007-06-23 | 
Enrico Tassi | removed ugly printings | 
commit | commitdiff | tree | snapshot | 
| 2007-06-21 | 
Wilmer Ricciotti | PoplMark challenge part 1a: new, shorter version w...  | 
commit | commitdiff | tree | snapshot | 
| 2007-06-21 | 
Enrico Tassi | better description | 
commit | commitdiff | tree | snapshot | 
| 2007-06-21 | 
Enrico Tassi | better description | 
commit | commitdiff | tree | snapshot | 
| 2007-06-21 | 
Enrico Tassi | here we are, a version that compiles and seems to run | 
commit | commitdiff | tree | snapshot | 
| 2007-06-14 | 
Claudio Sacerdoti...  | Incompatible syntax problem between MySql e Sqlite3...  | 
commit | commitdiff | tree | snapshot | 
| 2007-06-13 | 
Enrico Tassi | cut is now implemented building a letin and not a beta...  | 
commit | commitdiff | tree | snapshot | 
| 2007-06-13 | 
Enrico Tassi | many changes: | 
commit | commitdiff | tree | snapshot | 
| 2007-06-06 | 
Enrico Tassi | sort_new_elems on prop_only | 
commit | commitdiff | tree | snapshot | 
| 2007-06-06 | 
Enrico Tassi | fixed to allow make-dist | 
commit | commitdiff | tree | snapshot | 
| 2007-06-06 | 
Enrico Tassi | added doc for compose | 
commit | commitdiff | tree | snapshot | 
| 2007-06-06 | 
Enrico Tassi | compose now returns a good metasenv | 
commit | commitdiff | tree | snapshot | 
| 2007-06-04 | 
Enrico Tassi | tentative fix | 
commit | commitdiff | tree | snapshot | 
| 2007-06-04 | 
Claudio Sacerdoti...  | Another optimization, already done for geq. | 
commit | commitdiff | tree | snapshot | 
| 2007-06-04 | 
Enrico Tassi | auto proof are printed in procedural style | 
commit | commitdiff | tree | snapshot | 
| 2007-06-04 | 
Enrico Tassi | new more flexible compose, see matita/tests/compose...  | 
commit | commitdiff | tree | snapshot | 
| 2007-06-02 | 
Enrico Tassi | wrong assertion was inserted, now just a warning to...  | 
commit | commitdiff | tree | snapshot | 
| 2007-06-01 | 
Claudio Sacerdoti...  | Some interesting optimizations to prevent many bad...  | 
commit | commitdiff | tree | snapshot | 
| 2007-06-01 | 
Claudio Sacerdoti...  | Profiling enabled again. | 
commit | commitdiff | tree | snapshot | 
| 2007-06-01 | 
Enrico Tassi | removed some refinement_toolkit | 
commit | commitdiff | tree | snapshot | 
| 2007-06-01 | 
Enrico Tassi | new compose tactic, still undocumented. | 
commit | commitdiff | tree | snapshot | 
| 2007-06-01 | 
Claudio Sacerdoti...  | I do not know why, but | 
commit | commitdiff | tree | snapshot | 
| 2007-06-01 | 
Enrico Tassi | hacks for paramodulation declarative proofs | 
commit | commitdiff | tree | snapshot | 
| 2007-05-31 | 
Claudio Sacerdoti...  | Final (???) bug fixed. | 
commit | commitdiff | tree | snapshot | 
| 2007-05-31 | 
Claudio Sacerdoti...  | DOOMSDAY 1.0: | 
commit | commitdiff | tree | snapshot | 
| 2007-05-31 | 
Claudio Sacerdoti...  | Bug fixed: wrong id. | 
commit | commitdiff | tree | snapshot | 
| 2007-05-31 | 
Claudio Sacerdoti...  | Ferruccio has changed the semantics of the old ~pattern...  | 
commit | commitdiff | tree | snapshot | 
| 2007-05-31 | 
Claudio Sacerdoti...  | More exceptions pretty-printed. | 
commit | commitdiff | tree | snapshot | 
| next |