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 |
2007-05-30 |
Claudio Sacerdoti... | theory_explorer now communicates directly with matitawi... |
commit | commitdiff | tree | snapshot |
2007-05-30 |
Enrico Tassi | now the window can be closed also using X |
commit | commitdiff | tree | snapshot |
2007-05-29 |
Claudio Sacerdoti... | 1. Profiling enabled. |
commit | commitdiff | tree | snapshot |
2007-05-29 |
Enrico Tassi | hSqlite3.ml used create_fun_2 to define REGEXP. |
commit | commitdiff | tree | snapshot |
2007-05-29 |
Enrico Tassi | added some lines to compile for debugging |
commit | commitdiff | tree | snapshot |
2007-05-29 |
Enrico Tassi | added pruning option in autogui |
commit | commitdiff | tree | snapshot |
2007-05-29 |
Andrea Asperti | Corrected version od meta_convertibnility_subst. |
commit | commitdiff | tree | snapshot |
2007-05-28 |
Claudio Sacerdoti... | Bug fixed (hopefully without introducing new ones)... |
commit | commitdiff | tree | snapshot |
2007-05-28 |
Andrea Asperti | Improved pruning (no propress). |
commit | commitdiff | tree | snapshot |
2007-05-28 |
Andrea Asperti | Added a new version of meta_convertibnility that return... |
commit | commitdiff | tree | snapshot |
2007-05-26 |
Claudio Sacerdoti... | 1. Now I save a log.ma file that is exactly what is... |
commit | commitdiff | tree | snapshot |
2007-05-26 |
Claudio Sacerdoti... | log.ma is now created. But it does not contain the... |
commit | commitdiff | tree | snapshot |
2007-05-25 |
Claudio Sacerdoti... | log.ma is now created. It records all the tests (both... |
commit | commitdiff | tree | snapshot |
2007-05-25 |
Claudio Sacerdoti... | Yet another assert failure fixed. |
commit | commitdiff | tree | snapshot |
2007-05-25 |
Claudio Sacerdoti... | More warnings. |
commit | commitdiff | tree | snapshot |
2007-05-25 |
Enrico Tassi | added $Revision$ |
commit | commitdiff | tree | snapshot |
2007-05-25 |
Enrico Tassi | auto --> autobatch |
commit | commitdiff | tree | snapshot |
2007-05-25 |
Enrico Tassi | auto --> autobatch |
commit | commitdiff | tree | snapshot |
2007-05-24 |
Claudio Sacerdoti... | New asserts. |
commit | commitdiff | tree | snapshot |
2007-05-24 |
Enrico Tassi | auto and autogui... some work |
commit | commitdiff | tree | snapshot |
2007-05-24 |
Enrico Tassi | auto and autogui... some work |
commit | commitdiff | tree | snapshot |
2007-05-24 |
Enrico Tassi | fixed a when that was causing backtrace loss |
commit | commitdiff | tree | snapshot |
2007-05-24 |
Claudio Sacerdoti... | More assert failures and some bugs (detected by assert... |
commit | commitdiff | tree | snapshot |
2007-05-24 |
Enrico Tassi | added some flags to render subproofs (an hack) |
commit | commitdiff | tree | snapshot |
2007-05-24 |
Claudio Sacerdoti... | All known bugs fixed. |
commit | commitdiff | tree | snapshot |
2007-05-24 |
Claudio Sacerdoti... | It no longer generates double arcs between nodes. |
commit | commitdiff | tree | snapshot |
2007-05-24 |
Claudio Sacerdoti... | Still bugged. |
commit | commitdiff | tree | snapshot |
2007-05-24 |
Claudio Sacerdoti... | theory_explorer_do_not_trust_auto.ml is the version... |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Claudio Sacerdoti... | I am now using tred to remove transitive dependencies... |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Claudio Sacerdoti... | 1. generation of log file commented out (it gets too... |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Claudio Sacerdoti... | Yet another patch to LibraryClean. |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Claudio Sacerdoti... | HSql.Error ==> HSql.Error of string |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Claudio Sacerdoti... | prerr_endine ==> debug_print everywhere |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Claudio Sacerdoti... | Reindented. |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Claudio Sacerdoti... | Even more color (for new nodes). |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Enrico Tassi | deps fixed |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Claudio Sacerdoti... | Use different colors to understand what is going on. |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Enrico Tassi | makefile reworked to make debian package possible |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Claudio Sacerdoti... | Unlinked nodes are now printed. |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Enrico Tassi | made matita.runtime_base_dir overridable setting MATITA... |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Enrico Tassi | MATITA_* env variable preserved when publishing a devel... |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Enrico Tassi | changed the way environment variable can interfere... |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Enrico Tassi | added is_writabledir to extlib |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Enrico Tassi | added some hacks for the debian package |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Enrico Tassi | debian package for matita |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Claudio Sacerdoti... | xxx.dot improved |
commit | commitdiff | tree | snapshot |
2007-05-23 |
Claudio Sacerdoti... | Automatic exploration of the theory of intuitionistic... |
commit | commitdiff | tree | snapshot |
2007-05-22 |
Claudio Sacerdoti... | Slightly more efficient patch. |
commit | commitdiff | tree | snapshot |
2007-05-20 |
Ferruccio Guidi | applyTransformation: added debugging information |
commit | commitdiff | tree | snapshot |
next |