]> matita.cs.unibo.it Git - helm.git/history - matita/library
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
rc-1
[helm.git] / matita / library /
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
2006-06-15 Andrea Aspertiexamples of applyS tree | commitdiff
2006-06-14 Stefano Zacchirolifixed bad spellend "stantard" tree | commitdiff
2006-06-09 Claudio Sacerdoti... 1. the default for the default equality/absurd/true... tree | commitdiff
2006-06-09 Andrea AspertiNotation for congruent. tree | commitdiff
2006-05-25 Enrico Tassiadded a file useful to load all notation tree | commitdiff
2006-05-09 Enrico Tassitypes2006 patch tree | commitdiff
2006-04-12 Enrico Tassiexported pp function for terms tree | commitdiff
2006-03-17 Enrico Tassitests are now handled with a standard Makefile that... tree | commitdiff
2006-03-16 Enrico Tassione more step toward release and bench reorganization tree | commitdiff
2006-03-15 Enrico Tassisnapshot for release tree | commitdiff
2006-03-13 Enrico TassiHuge commit for the release. Includes: tree | commitdiff
2006-03-07 Claudio Sacerdoti... This simplify seems to diverge! tree | commitdiff
2006-03-07 Claudio Sacerdoti... First theorems proved on left cosets. tree | commitdiff
2006-02-23 Claudio Sacerdoti... 64 "change" here and there in the library are now simpl... tree | commitdiff
2006-02-22 Claudio Sacerdoti... simplify used in place of change tree | commitdiff
2006-02-22 Claudio Sacerdoti... Bug fixed in simplify: delta expansion of constants... tree | commitdiff
2006-02-21 Claudio Sacerdoti... Coercions are now hidden by default (in termAcicContent.ml) tree | commitdiff
2006-02-20 Claudio Sacerdoti... Finished one lemma (after many bug fixes here and there). tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.