]> matita.cs.unibo.it Git - helm.git/history - helm/software/matita/library
More exceptions pretty-printed.
[helm.git] / helm / software / matita / library /
2007-05-24 Enrico Tassiauto and autogui... some work
2007-05-20 Ferruccio GuidiapplyTransformation: added debugging information
2007-05-17 Enrico Tassiauto rewritten with only one tail recursive function.
2007-05-09 Andrea AspertiA few extensions for the moebius inversion theorem
2007-05-09 Andrea AspertiProof of the moebius inversion theorem
2007-04-20 Claudio Sacerdoti... Much ado about nothing:
2007-04-18 Enrico Tassimore discriminate
2007-04-16 Enrico Tassibetter simplify
2007-04-16 Enrico Tassiclosed all axioms
2007-04-10 Enrico Tassiset -> type
2007-04-10 Enrico Tassi...
2007-04-10 Enrico Tassi...
2007-04-03 Enrico Tassinew case implementation
2007-04-02 Enrico Tassiadded some tests for cases
2007-03-26 Enrico Tassiadded eta expansion to avoid universe inconsistency.
2007-03-16 Andrea AspertiNew contrib moebius.ma.
2007-03-16 Andrea AspertiExtensions required for the moebius function (in Z).
2007-03-13 Andrea AspertiFew theorems added.`
2007-03-13 Andrea Aspertinew version of div_and_mod
2007-02-08 Claudio Sacerdoti... More progress in technicalities/setoids.ma.
2007-02-08 Claudio Sacerdoti... * 'default "equality"' command changed to consider...
2007-02-06 Claudio Sacerdoti... More stuff in technicalities/setoids.ma
2007-02-01 Enrico Tassirestored coercions between eq and eq
2007-01-30 Claudio Sacerdoti... Proof size nicely reduced using distributive branching...
2007-01-30 Claudio Sacerdoti... Even more (painful) work on setoids.
2007-01-29 Claudio Sacerdoti... More work on setoids.
2007-01-29 Claudio Sacerdoti... Some more datatypes lifted to Type.
2007-01-27 Claudio Sacerdoti... Added option datatype. Required (for technicalities...
2007-01-18 Wilmer Ricciottinew version, using new tacticals
2007-01-16 Andrea AspertiAdded SetoidInc.m
2007-01-16 Andrea AspertiSome CoRN files.
2007-01-07 Claudio Sacerdoti... Porting of setoids.ma from Coq continued.
2007-01-07 Claudio Sacerdoti... Bug fixed in definition of cic:/.../setoids/make_compat...
2006-12-29 Claudio Sacerdoti... eq_ind' generalized to eq_rect'
2006-12-22 Ferruccio Guidilegacy development created
2006-12-18 Andrea AspertiM logic/coimplication.ma
2006-12-18 Andrea AspertiRenamed iterative into map_iter_p and moved around...
2006-12-18 Andrea AspertiProof of Euler theorem.
2006-12-08 Ferruccio Guidinew makefiles
2006-12-06 Claudio Sacerdoti... More simplification using better notation.
2006-12-01 Ferruccio Guidisome uris fixed
2006-11-30 Claudio Sacerdoti... Notation \middot used everywhere in place of *.
2006-11-30 Claudio Sacerdoti... I have changed the nice notation for derivatives a...
2006-11-30 Claudio Sacerdoti... Added a demo for Matita: two slightly different proofs...
2006-11-30 Wilmer Ricciottilibrary/Fsub: minor fix
2006-11-30 Wilmer Ricciottilibrary: added solution to POPLMark challenge part...
2006-11-29 Ferruccio Guidi- new library/logic/coimplication.ma uses new decompose...
2006-11-27 Andrea AspertiMatita's default equality has changed
2006-11-27 Andrea AspertiSmall changes
2006-11-23 Andrea AspertiFixed a call to auto, and commented the remaining part.
2006-11-23 Andrea Aspertiparamodulation removed
2006-11-23 Andrea AspertiMinor changes.
2006-11-23 Andrea AspertiSimplified version.
2006-11-23 Andrea AspertiAdding CoRN.
2006-11-15 Ferruccio Guidifixed base uri
2006-11-15 Andrea Aspertilt_O_S moved to nat/orders.ma
2006-11-15 Andrea AspertiAdded lt_O_S.
2006-10-30 Andrea Aspertilibrary = yes!
2006-10-25 Claudio Sacerdoti... Our unification used to guess a very complex argument...
2006-10-09 Claudio Sacerdoti... added to applyS in nat/gcd.ma a timeout large enough...
2006-10-09 Andrea AspertiThe two coercions sym_eq e eq_f gives BIG TROUBLES...
2006-10-06 Enrico Tassiresumed ol auto
2006-10-03 Enrico Tassicommented out are_convertible in is_identity
2006-10-02 Enrico Tassiremoved a pointless call to auto
2006-09-29 Enrico Tassirestored the good factorization file
2006-09-27 Enrico Tassi...
2006-09-27 Claudio Sacerdoti... More work on the translation of technicalities/setoids.ma.
2006-09-27 Claudio Sacerdoti... Initial work on setoids:
2006-09-27 Claudio Sacerdoti... Initial work on setoids:
2006-09-26 Claudio Sacerdoti... {discriminate,injection} => destruct
2006-09-21 Enrico Tassiauto snapshot
2006-09-21 Enrico Tassiadded notation
2006-09-04 Enrico TassiBIG FAT COMMIT REGARDING COERCIONS:
2006-08-29 Ferruccio Guidialiases removed
2006-08-28 Ferruccio Guidi- Level-1: some problems solved
2006-08-27 Ferruccio Guidi- Level-1: added two problems
2006-08-26 Ferruccio Guidi- Level-1: added some problems
2006-08-26 Ferruccio Guidi- added some aliases
2006-07-27 maiorinoNotation for the existential quantifier moved to core_n...
2006-07-26 Stefano Zacchiroliadded tinycals to the proof we frequently use for examp...
2006-07-25 Enrico Tassiadded definition of f_equal1. I think this file should...
2006-07-24 Andrea AspertiA compiling version of the library.
2006-07-24 Stefano Zacchiroliadded missing dependency
2006-07-24 Stefano Zacchiroliequality now requires 2 extra parameters
2006-07-24 Stefano Zacchiroliremoved reference to primes1.ma (now removed)
2006-07-20 Enrico Tassireorganization
2006-07-11 Enrico Tassifixed
2006-07-10 Enrico Tassirenamed the coercion
2006-07-06 Enrico Tassieq_f1
2006-07-06 Enrico Tassimegatheorem (even if unused)
2006-06-28 Enrico Tassicsc trick on steroids
2006-06-15 Andrea Aspertiexamples of applyS
2006-06-14 Stefano Zacchirolifixed bad spellend "stantard"
2006-06-09 Claudio Sacerdoti... 1. the default for the default equality/absurd/true...
2006-06-09 Andrea AspertiNotation for congruent.
2006-05-25 Enrico Tassiadded a file useful to load all notation
2006-05-09 Enrico Tassitypes2006 patch
2006-04-12 Enrico Tassiexported pp function for terms
2006-03-17 Enrico Tassitests are now handled with a standard Makefile that...
2006-03-16 Enrico Tassione more step toward release and bench reorganization
next