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 |
2007-04-10 |
Enrico Tassi | ... |
tree | commitdiff |
2007-04-10 |
Enrico Tassi | ... |
tree | commitdiff |
2007-04-03 |
Enrico Tassi | new case implementation |
tree | commitdiff |
2007-04-02 |
Enrico Tassi | added some tests for cases |
tree | commitdiff |
2007-03-26 |
Enrico Tassi | added eta expansion to avoid universe inconsistency. |
tree | commitdiff |
2007-03-16 |
Andrea Asperti | New contrib moebius.ma. |
tree | commitdiff |
2007-03-16 |
Andrea Asperti | Extensions required for the moebius function (in Z). |
tree | commitdiff |
2007-03-13 |
Andrea Asperti | Few theorems added.` |
tree | commitdiff |
2007-03-13 |
Andrea Asperti | new version of div_and_mod |
tree | commitdiff |
2007-02-08 |
Claudio Sacerdoti... | More progress in technicalities/setoids.ma. |
tree | commitdiff |
2007-02-08 |
Claudio Sacerdoti... | * 'default "equality"' command changed to consider... |
tree | commitdiff |
2007-02-06 |
Claudio Sacerdoti... | More stuff in technicalities/setoids.ma |
tree | commitdiff |
2007-02-01 |
Enrico Tassi | restored coercions between eq and eq |
tree | commitdiff |
2007-01-30 |
Claudio Sacerdoti... | Proof size nicely reduced using distributive branching... |
tree | commitdiff |
2007-01-30 |
Claudio Sacerdoti... | Even more (painful) work on setoids. |
tree | commitdiff |
2007-01-29 |
Claudio Sacerdoti... | More work on setoids. |
tree | commitdiff |
2007-01-29 |
Claudio Sacerdoti... | Some more datatypes lifted to Type. |
tree | commitdiff |
2007-01-27 |
Claudio Sacerdoti... | Added option datatype. Required (for technicalities... |
tree | commitdiff |
2007-01-18 |
Wilmer Ricciotti | new version, using new tacticals |
tree | commitdiff |
2007-01-16 |
Andrea Asperti | Added SetoidInc.m |
tree | commitdiff |
2007-01-16 |
Andrea Asperti | Some CoRN files. |
tree | commitdiff |
2007-01-07 |
Claudio Sacerdoti... | Porting of setoids.ma from Coq continued. |
tree | commitdiff |
2007-01-07 |
Claudio Sacerdoti... | Bug fixed in definition of cic:/.../setoids/make_compat... |
tree | commitdiff |
2006-12-29 |
Claudio Sacerdoti... | eq_ind' generalized to eq_rect' |
tree | commitdiff |
2006-12-22 |
Ferruccio Guidi | legacy development created |
tree | commitdiff |
2006-12-18 |
Andrea Asperti | M logic/coimplication.ma |
tree | commitdiff |
2006-12-18 |
Andrea Asperti | Renamed iterative into map_iter_p and moved around... |
tree | commitdiff |
2006-12-18 |
Andrea Asperti | Proof of Euler theorem. |
tree | commitdiff |
2006-12-08 |
Ferruccio Guidi | new makefiles |
tree | commitdiff |
2006-12-06 |
Claudio Sacerdoti... | More simplification using better notation. |
tree | commitdiff |
2006-12-01 |
Ferruccio Guidi | some uris fixed |
tree | commitdiff |
2006-11-30 |
Claudio Sacerdoti... | Notation \middot used everywhere in place of *. |
tree | commitdiff |
2006-11-30 |
Claudio Sacerdoti... | I have changed the nice notation for derivatives a... |
tree | commitdiff |
2006-11-30 |
Claudio Sacerdoti... | Added a demo for Matita: two slightly different proofs... |
tree | commitdiff |
2006-11-30 |
Wilmer Ricciotti | library/Fsub: minor fix |
tree | commitdiff |
2006-11-30 |
Wilmer Ricciotti | library: added solution to POPLMark challenge part... |
tree | commitdiff |
2006-11-29 |
Ferruccio Guidi | - new library/logic/coimplication.ma uses new decompose... |
tree | commitdiff |
2006-11-27 |
Andrea Asperti | Matita's default equality has changed |
tree | commitdiff |
2006-11-27 |
Andrea Asperti | Small changes |
tree | commitdiff |
2006-11-23 |
Andrea Asperti | Fixed a call to auto, and commented the remaining part. |
tree | commitdiff |
2006-11-23 |
Andrea Asperti | paramodulation removed |
tree | commitdiff |
2006-11-23 |
Andrea Asperti | Minor changes. |
tree | commitdiff |
2006-11-23 |
Andrea Asperti | Simplified version. |
tree | commitdiff |
2006-11-23 |
Andrea Asperti | Adding CoRN. |
tree | commitdiff |
2006-11-15 |
Ferruccio Guidi | fixed base uri |
tree | commitdiff |
2006-11-15 |
Andrea Asperti | lt_O_S moved to nat/orders.ma |
tree | commitdiff |
2006-11-15 |
Andrea Asperti | Added lt_O_S. |
tree | commitdiff |
2006-10-30 |
Andrea Asperti | library = yes! |
tree | commitdiff |
2006-10-25 |
Claudio Sacerdoti... | Our unification used to guess a very complex argument... |
tree | commitdiff |
2006-10-09 |
Claudio Sacerdoti... | added to applyS in nat/gcd.ma a timeout large enough... |
tree | commitdiff |
2006-10-09 |
Andrea Asperti | The two coercions sym_eq e eq_f gives BIG TROUBLES... |
tree | commitdiff |
2006-10-06 |
Enrico Tassi | resumed ol auto |
tree | commitdiff |
2006-10-03 |
Enrico Tassi | commented out are_convertible in is_identity |
tree | commitdiff |
2006-10-02 |
Enrico Tassi | removed a pointless call to auto |
tree | commitdiff |
2006-09-29 |
Enrico Tassi | restored the good factorization file |
tree | commitdiff |
2006-09-27 |
Enrico Tassi | ... |
tree | commitdiff |
2006-09-27 |
Claudio Sacerdoti... | More work on the translation of technicalities/setoids.ma. |
tree | commitdiff |
2006-09-27 |
Claudio Sacerdoti... | Initial work on setoids: |
tree | commitdiff |
2006-09-27 |
Claudio Sacerdoti... | Initial work on setoids: |
tree | commitdiff |
2006-09-26 |
Claudio Sacerdoti... | {discriminate,injection} => destruct |
tree | commitdiff |
2006-09-21 |
Enrico Tassi | auto snapshot |
tree | commitdiff |
2006-09-21 |
Enrico Tassi | added notation |
tree | commitdiff |
2006-09-04 |
Enrico Tassi | BIG FAT COMMIT REGARDING COERCIONS: |
tree | commitdiff |
2006-08-29 |
Ferruccio Guidi | aliases removed |
tree | commitdiff |
2006-08-28 |
Ferruccio Guidi | - Level-1: some problems solved |
tree | commitdiff |
2006-08-27 |
Ferruccio Guidi | - Level-1: added two problems |
tree | commitdiff |
2006-08-26 |
Ferruccio Guidi | - Level-1: added some problems |
tree | commitdiff |
next |