| 2007-07-16 |
Wilmer Ricciotti | corrected axiom mod_plus |
tree | commitdiff |
| 2007-07-14 |
Ferruccio Guidi | new definitions and new theorems |
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... | Last crazy commit reverted. |
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-11 |
Claudio Sacerdoti... | auto new => autobatch |
tree | commitdiff |
| 2007-07-11 |
Claudio Sacerdoti... | auto new => autobatch |
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-10 |
Enrico Tassi | ... |
tree | commitdiff |
| 2007-07-09 |
Enrico Tassi | 1. bug fixed in tick |
tree | commitdiff |
| 2007-07-09 |
Enrico Tassi | signal hadler restored after runnig external 'make' |
tree | commitdiff |
| 2007-07-09 |
Claudio Sacerdoti... | Interesting theorem added (but still to be proved). |
tree | commitdiff |
| 2007-07-09 |
Enrico Tassi | added few more fun to this test |
tree | commitdiff |
| 2007-07-09 |
Enrico Tassi | auto->autobatch |
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 |
Ferruccio Guidi | some old auto yurned into autobatch |
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-06-13 |
Enrico Tassi | many changes: |
tree | commitdiff |
| 2007-06-06 |
Enrico Tassi | fixed to allow make-dist |
tree | commitdiff |
| 2007-06-06 |
Enrico Tassi | added doc for compose |
tree | commitdiff |
| 2007-06-04 |
Enrico Tassi | tentative fix |
tree | commitdiff |
| 2007-06-04 |
Claudio Sacerdoti... | Another optimization, already done for geq. |
tree | commitdiff |
| 2007-06-04 |
Enrico Tassi | auto proof are printed in procedural style |
tree | commitdiff |
| 2007-06-04 |
Enrico Tassi | new more flexible compose, see matita/tests/compose... |
tree | commitdiff |
| 2007-06-01 |
Claudio Sacerdoti... | Some interesting optimizations to prevent many bad... |
tree | commitdiff |
| 2007-06-01 |
Claudio Sacerdoti... | Profiling enabled again. |
tree | commitdiff |
| 2007-06-01 |
Enrico Tassi | new compose tactic, still undocumented. |
tree | commitdiff |
| 2007-06-01 |
Claudio Sacerdoti... | I do not know why, but |
tree | commitdiff |
| 2007-06-01 |
Enrico Tassi | hacks for paramodulation declarative proofs |
tree | commitdiff |
| 2007-05-31 |
Claudio Sacerdoti... | Final (???) bug fixed. |
tree | commitdiff |
| 2007-05-31 |
Claudio Sacerdoti... | More exceptions pretty-printed. |
tree | commitdiff |
| 2007-05-30 |
Claudio Sacerdoti... | theory_explorer now communicates directly with matitawi... |
tree | commitdiff |
| 2007-05-30 |
Enrico Tassi | now the window can be closed also using X |
tree | commitdiff |
| 2007-05-29 |
Claudio Sacerdoti... | 1. Profiling enabled. |
tree | commitdiff |
| 2007-05-29 |
Enrico Tassi | hSqlite3.ml used create_fun_2 to define REGEXP. |
tree | commitdiff |
| 2007-05-29 |
Enrico Tassi | added some lines to compile for debugging |
tree | commitdiff |
| 2007-05-29 |
Enrico Tassi | added pruning option in autogui |
tree | commitdiff |
| 2007-05-26 |
Claudio Sacerdoti... | 1. Now I save a log.ma file that is exactly what is... |
tree | commitdiff |
| 2007-05-26 |
Claudio Sacerdoti... | log.ma is now created. But it does not contain the... |
tree | commitdiff |
| 2007-05-25 |
Claudio Sacerdoti... | log.ma is now created. It records all the tests (both... |
tree | commitdiff |
| 2007-05-25 |
Claudio Sacerdoti... | Yet another assert failure fixed. |
tree | commitdiff |
| 2007-05-25 |
Claudio Sacerdoti... | More warnings. |
tree | commitdiff |
| 2007-05-25 |
Enrico Tassi | auto --> autobatch |
tree | commitdiff |
| 2007-05-25 |
Enrico Tassi | auto --> autobatch |
tree | commitdiff |
| 2007-05-24 |
Claudio Sacerdoti... | New asserts. |
tree | commitdiff |
| 2007-05-24 |
Enrico Tassi | auto and autogui... some work |
tree | commitdiff |
| 2007-05-24 |
Claudio Sacerdoti... | More assert failures and some bugs (detected by assert... |
tree | commitdiff |
| 2007-05-24 |
Claudio Sacerdoti... | All known bugs fixed. |
tree | commitdiff |
| 2007-05-24 |
Claudio Sacerdoti... | It no longer generates double arcs between nodes. |
tree | commitdiff |
| 2007-05-24 |
Claudio Sacerdoti... | Still bugged. |
tree | commitdiff |
| 2007-05-24 |
Claudio Sacerdoti... | theory_explorer_do_not_trust_auto.ml is the version... |
tree | commitdiff |
| 2007-05-23 |
Claudio Sacerdoti... | I am now using tred to remove transitive dependencies... |
tree | commitdiff |
| 2007-05-23 |
Claudio Sacerdoti... | 1. generation of log file commented out (it gets too... |
tree | commitdiff |
| 2007-05-23 |
Claudio Sacerdoti... | Even more color (for new nodes). |
tree | commitdiff |
| 2007-05-23 |
Enrico Tassi | deps fixed |
tree | commitdiff |
| 2007-05-23 |
Claudio Sacerdoti... | Use different colors to understand what is going on. |
tree | commitdiff |
| 2007-05-23 |
Enrico Tassi | makefile reworked to make debian package possible |
tree | commitdiff |
| 2007-05-23 |
Claudio Sacerdoti... | Unlinked nodes are now printed. |
tree | commitdiff |
| 2007-05-23 |
Enrico Tassi | made matita.runtime_base_dir overridable setting MATITA... |
tree | commitdiff |
| 2007-05-23 |
Enrico Tassi | MATITA_* env variable preserved when publishing a devel... |
tree | commitdiff |
| 2007-05-23 |
Claudio Sacerdoti... | xxx.dot improved |
tree | commitdiff |
| 2007-05-23 |
Claudio Sacerdoti... | Automatic exploration of the theory of intuitionistic... |
tree | commitdiff |
| 2007-05-20 |
Ferruccio Guidi | applyTransformation: added debugging information |
tree | commitdiff |
| 2007-05-18 |
Ferruccio Guidi | - new devel contribs/LAMBDA-TYPES/Base-2 with the autom... |
tree | commitdiff |
| 2007-05-17 |
Enrico Tassi | added a (for the moment) dummy field _subst to Proofeng... |
tree | commitdiff |
| 2007-05-17 |
Enrico Tassi | auto rewritten with only one tail recursive function. |
tree | commitdiff |
| 2007-05-17 |
Enrico Tassi | OPT tests restored |
tree | commitdiff |
| 2007-05-13 |
Ferruccio Guidi | library-auto removed from tests (too slow even in nativ... |
tree | commitdiff |
| 2007-05-09 |
Ferruccio Guidi | PrimitiveTactics: intros _ now aveilable |
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-05-03 |
Ferruccio Guidi | library-auto is only tested in native code (in byte... |
tree | commitdiff |
| 2007-05-02 |
Ferruccio Guidi | some improvements |
tree | commitdiff |
| 2007-05-01 |
Ferruccio Guidi | SubstTactic: bug fix |
tree | commitdiff |
| 2007-04-28 |
Ferruccio Guidi | AMBDA-TYPES: some improvements. subst now fully exploited |
tree | commitdiff |
| 2007-04-27 |
Ferruccio Guidi | LAMBDA-TYPES: some improvements |
tree | commitdiff |
| 2007-04-26 |
Ferruccio Guidi | procedural: bug fixes |
tree | commitdiff |
| 2007-04-24 |
Claudio Sacerdoti... | goal ==> focus |
tree | commitdiff |
| 2007-04-23 |
Claudio Sacerdoti... | Deprecated "goal" removed. |
tree | commitdiff |
| 2007-04-20 |
Claudio Sacerdoti... | A new test on some non punctuation tacticals. |
tree | commitdiff |
| 2007-04-20 |
Claudio Sacerdoti... | added skip, removed end |
tree | commitdiff |
| next |
projects / helm.git / history