]> matita.cs.unibo.it Git - helm.git/history - matita/library
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
List.ma: added function nth (with default value in case of failure)
[helm.git] / matita / library /
2007-07-04 Claudio Sacerdoti... List.ma: added function nth (with default value in... tree | commitdiff
2007-06-30 Cristian ArmentanoNew definition of Euler's totient function. tree | commitdiff
2007-06-29 Cristian Armentanogeneric version, specializing generic_sigma_p.ma tree | commitdiff
2007-06-29 Cristian Armentanogeneric version tree | commitdiff
2007-06-29 Cristian Armentanotheorems about sigma_p proved using sigma_p_gen tree | commitdiff
2007-06-27 Cristian Armentanonew gcd properties, and theorems for totient, and theor... tree | commitdiff
2007-06-26 Cristian Armentano(no commit message) tree | commitdiff
2007-06-26 Cristian Armentanogeneric sommatory. tree | commitdiff
2007-06-21 Wilmer RicciottiPoplMark challenge part 1a: new, shorter version w... tree | commitdiff
2007-05-24 Enrico Tassiauto and autogui... some work tree | commitdiff
2007-05-20 Ferruccio GuidiapplyTransformation: added debugging information tree | commitdiff
2007-05-17 Enrico Tassiauto rewritten with only one tail recursive function. tree | commitdiff
2007-05-09 Andrea AspertiA few extensions for the moebius inversion theorem tree | commitdiff
2007-05-09 Andrea AspertiProof of the moebius inversion theorem tree | commitdiff
2007-04-20 Claudio Sacerdoti... Much ado about nothing: tree | commitdiff
2007-04-18 Enrico Tassimore discriminate tree | commitdiff
2007-04-16 Enrico Tassibetter simplify tree | commitdiff
2007-04-16 Enrico Tassiclosed all axioms tree | commitdiff
2007-04-10 Enrico Tassiset -> type tree | commitdiff
2007-04-10 Enrico Tassi... tree | commitdiff
2007-04-10 Enrico Tassi... tree | commitdiff
2007-04-03 Enrico Tassinew case implementation tree | commitdiff
2007-04-02 Enrico Tassiadded some tests for cases tree | commitdiff
2007-03-26 Enrico Tassiadded eta expansion to avoid universe inconsistency. tree | commitdiff
2007-03-16 Andrea AspertiNew contrib moebius.ma. tree | commitdiff
2007-03-16 Andrea AspertiExtensions required for the moebius function (in Z). tree | commitdiff
2007-03-13 Andrea AspertiFew theorems added.` tree | commitdiff
2007-03-13 Andrea Aspertinew 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 Tassirestored 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 Ricciottinew version, using new tacticals tree | commitdiff
2007-01-16 Andrea AspertiAdded SetoidInc.m tree | commitdiff
2007-01-16 Andrea AspertiSome 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 Guidilegacy development created tree | commitdiff
2006-12-18 Andrea AspertiM logic/coimplication.ma tree | commitdiff
2006-12-18 Andrea AspertiRenamed iterative into map_iter_p and moved around... tree | commitdiff
2006-12-18 Andrea AspertiProof of Euler theorem. tree | commitdiff
2006-12-08 Ferruccio Guidinew makefiles tree | commitdiff
2006-12-06 Claudio Sacerdoti... More simplification using better notation. tree | commitdiff
2006-12-01 Ferruccio Guidisome 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 Ricciottilibrary/Fsub: minor fix tree | commitdiff
2006-11-30 Wilmer Ricciottilibrary: 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 AspertiMatita's default equality has changed tree | commitdiff
2006-11-27 Andrea AspertiSmall changes tree | commitdiff
2006-11-23 Andrea AspertiFixed a call to auto, and commented the remaining part. tree | commitdiff
2006-11-23 Andrea Aspertiparamodulation removed tree | commitdiff
2006-11-23 Andrea AspertiMinor changes. tree | commitdiff
2006-11-23 Andrea AspertiSimplified version. tree | commitdiff
2006-11-23 Andrea AspertiAdding CoRN. tree | commitdiff
2006-11-15 Ferruccio Guidifixed base uri tree | commitdiff
2006-11-15 Andrea Aspertilt_O_S moved to nat/orders.ma tree | commitdiff
2006-11-15 Andrea AspertiAdded lt_O_S. tree | commitdiff
2006-10-30 Andrea Aspertilibrary = 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 AspertiThe two coercions sym_eq e eq_f gives BIG TROUBLES... tree | commitdiff
2006-10-06 Enrico Tassiresumed ol auto tree | commitdiff
2006-10-03 Enrico Tassicommented out are_convertible in is_identity tree | commitdiff
2006-10-02 Enrico Tassiremoved a pointless call to auto tree | commitdiff
2006-09-29 Enrico Tassirestored 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 Tassiauto snapshot tree | commitdiff
2006-09-21 Enrico Tassiadded notation tree | commitdiff
2006-09-04 Enrico TassiBIG FAT COMMIT REGARDING COERCIONS: tree | commitdiff
2006-08-29 Ferruccio Guidialiases 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
2006-08-26 Ferruccio Guidi- added some aliases tree | commitdiff
2006-07-27 maiorinoNotation for the existential quantifier moved to core_n... tree | commitdiff
2006-07-26 Stefano Zacchiroliadded tinycals to the proof we frequently use for examp... tree | commitdiff
2006-07-25 Enrico Tassiadded definition of f_equal1. I think this file should... tree | commitdiff
2006-07-24 Andrea AspertiA compiling version of the library. tree | commitdiff
2006-07-24 Stefano Zacchiroliadded missing dependency tree | commitdiff
2006-07-24 Stefano Zacchiroliequality now requires 2 extra parameters tree | commitdiff
2006-07-24 Stefano Zacchiroliremoved reference to primes1.ma (now removed) tree | commitdiff
2006-07-20 Enrico Tassireorganization tree | commitdiff
2006-07-11 Enrico Tassifixed tree | commitdiff
2006-07-10 Enrico Tassirenamed the coercion tree | commitdiff
2006-07-06 Enrico Tassieq_f1 tree | commitdiff
2006-07-06 Enrico Tassimegatheorem (even if unused) tree | commitdiff
2006-06-28 Enrico Tassicsc trick on steroids tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.