Starting with inventory: 0000026699-d6c10fbb70f9a32405ef1d50774630189ab2af63f406f1453b2755e8b6b2ebf6 [TAG 0.6 Nils Anders Danielsson **20111227194340 Ignore-this: 2a7b42ee6c56ee2a9bfb81a1ae05ad5f ] hash: 0000018616-525c0dfcd01bec86d54aa63b7df4fdf36b73d715f8d0f1e10fe3a33eaf485d0d [Removed release-specific information. Nils Anders Danielsson **20111227195401 Ignore-this: ec5d8cd6e014686e902bcbc168466316 ] hash: 0000000612-5ccd539b418a58322390dc7b3ce1e3c53452dfe2c7db62e3725cb1da0a0bcfd5 [Modified the version ranges of some dependencies. Nils Anders Danielsson **20120103205601 Ignore-this: 9aef21de942688c7a268d35c78715538 ] hash: 0000000497-518a98d5243d1a5b7d666ff493055cbe170d6bf78808be47f3f9c1ac9c5a8bda [Inlined some helper functions. Nils Anders Danielsson **20120127132635 Ignore-this: f636ab597e504978033629ef1d9f47fe ] hash: 0000001969-fb0aa6e39b7df57cc67779e09f2c9e460136a53f594fac1883c7d1e513afcc08 [Cosmetic change. Nils Anders Danielsson **20120127132700 Ignore-this: 490f9fef88952773222104bbf6672f83 ] hash: 0000000287-a6b8b09f3be12d8e261d21acffffbedfe9bf88a89980340bc796b3c6ca8dee5a [Added readFiniteFile. Nils Anders Danielsson **20120218111803 Ignore-this: a14d41344042cf41a5438af1f9a111a3 ] hash: 0000003702-1f232b4196ae58dc044bac056e391ff1ac352bbcd6927ffc56160794272e6ebc [Updated the copyright year range. Nils Anders Danielsson **20120225110204 Ignore-this: 1caec758d1560c6f13c613d77fff6f39 ] hash: 0000000318-2b668fb42b9006392da923207564d2f43798169f67f359bcebab04d7b56b3d7d [Added postulated, partly computing quotients. Nils Anders Danielsson **20120225110453 Ignore-this: dd2535cbffd5dfd4140fb004529e7886 + Implemented by Thorsten Altenkirch, James Chapman and myself. ] hash: 0000006473-6ed66f3fb0c2eaec33337f218eb8fb5172a1e22073bd904e3ea2e4a5ca478744 [Added _≡⟨_⟩_. Nils Anders Danielsson **20120225212140 Ignore-this: a22270b495981c2de38fed71532453a6 ] hash: 0000004991-40ad219ffb38ba7b71aa57ab4d986eb640f9065dbe647e46397b2fd9ff05a894 [Added idempotent. Nils Anders Danielsson **20120306141152 Ignore-this: 25563e42aae9e0dde988bfde2721eb5c ] hash: 0000001346-1d8b3472265929b9815eb59658e7d525d45b0c0d79b76b6c12f947a9a1e06e9b [Added _⇓. Nils Anders Danielsson **20120308131926 Ignore-this: 94c881424a838498d14d27b142b05fe9 ] hash: 0000000299-680eeffe98a86313cc536f72d2096a7039ba01f81b70ef432f26fec2f726f26c [Added Category.Monad.Partiality.All. Nils Anders Danielsson **20120312105757 Ignore-this: 76cd481222bc410f2fb60270d86c14ed ] hash: 0000006900-9dcc8f763df78c61943682606d8cb4178f818fea3b8e26704b0abbb1160863b6 [Added type signature to comply with new occurs check (issue 585). Andreas Abel **20120313164937 Ignore-this: 4f31b727f23d550a3f44a2040fff5449 ] hash: 0000000365-35db817b44988081432c1839eaf251b41f8ed1e9cae7438f8329258dcd4489ef [Added the irrelevance axiom. Nils Anders Danielsson **20120417083117 Ignore-this: a68d5d3274638dd650162685450bb04f ] hash: 0000000867-138e76395f4603484c8be50e0a2caab423e250bc03ea35872d4a228a927760d6 [Added Data.List.Properties.reverse-map-commute Joachim Breitner **20120507085543 Ignore-this: d1db66bb52a59967678f32fb25fc1102 ] hash: 0000000828-ed64c85383c00cbd8d532a0df42c8d76abdd4682354845a370e85678306ad7b7 [Added reverse-involutive Joachim Breitner **20120507085637 Ignore-this: 3606402188de305375b876f6890ab927 ] hash: 0000000758-0ae05d997fe74723cb60643893fcbf8b8ed2830292f7ba3420a90cd462cee945 [Adapted Joachim's patches to my taste. Nils Anders Danielsson **20120507094643 Ignore-this: b17198b645624e3c45929d2deacceec9 ] hash: 0000000731-29d5530036471cd4fb737d33df75956f64649c8fcff31f6ea7650385fa0e8b43 [Listed Joachim Breitner as a contributor. Nils Anders Danielsson **20120507094709 Ignore-this: d9da0f49ef2fd60caa084670acbb1786 ] hash: 0000000803-64ba04e6a104e88efda17042a3ca2d6f119fab56ec1f513da3cea2aa238ec479 [Relation.Binary.Vec.Pointwise: generalise to REL where possible Liyang HU **20120316110801 Ignore-this: 8df37c48fba43fb25ca50ddd9434c4c9 ] hash: 0000003390-70fe22d8ef2568d99ab79c7e8a41a8b7bcad093fb651c97e314f1c715ce1a168 [Relation.Binary.Vec.Pointwise: decidable{,′} for Pointwise{,′} Liyang HU **20120316110822 Ignore-this: c9abfc4fefb59277eed9e44ff20a1445 + Bonus head and tail for Pointwise′ ] hash: 0000001696-2ed1394010791be2ba0c7b7c64e6b18bd7906030ee901e79e0f3bcd9a3f462d5 [Data.Vector.Properties: lookup and _[_]≔_ behave as expected Liyang HU **20120316110701 Ignore-this: c79fe10e54fa8def528e31d688a2f660 + lookup∘update : lookup i (xs [ i ]≔ x) ≡ x + lookup∘update′ : i ≢ j → lookup i (xs [ j ]≔ y) ≡ lookup i xs ] hash: 0000001205-0c51a9e9beb72838c896c3cc3bf358f0a1f56d39c6b51227a6291882ea5174b8 [Adapted Liyang's patches to my taste. Nils Anders Danielsson **20120507124800 Ignore-this: f23fcf7f8cba245225710a4a9b7a8162 ] hash: 0000014494-c67ce420c50276919643bfdd3c9d1fb588245d23c1d40f36e3e572e0eb4e5029 [Listed Liyang Hu as a contributor. Nils Anders Danielsson **20120507125057 Ignore-this: a0489a5fe536a9aa87c6d824f7400157 ] hash: 0000000724-fdf23e701f7ca75d0e14251e8f7bbf9fc0df6f8236ed84d5a04def43ff3141d1 [AVL routines: added map, insertWith, union, unionWith, unions, unionsWith noam.zeilberger@gmail.com**20120429110436 Ignore-this: f7707bda509d0bc5e48e62bea59b51fe ] hash: 0000002068-a6b637cf81858419c8a5d38b30420d9d0ed9b3fc8fd790b5cd746840cde1a18b [Listed Noam Zeilberger as a contributor. Nils Anders Danielsson **20120507131227 Ignore-this: 1d1e23eeab0dc822594a9825daea7ef9 ] hash: 0000000512-4857a4cff964097d62d09da3270d5f00ab0039f22d4d01d77d71b1fe36f6cab5 [Adapted Noam's patch to my taste and fixed a bug. Nils Anders Danielsson **20120507150822 Ignore-this: 9b7fcfa80e62040e25a97548fb7d1af5 ] hash: 0000004460-d20dac75ecd143f06d70e334c320adf7af63d73d2c4530a7454d83a1791fa41e [primality implies coprimality gergo@erdi.hu**20120506122635 Ignore-this: a65431b2fa4a0d976f6fd4ab81cb8e7c Proof that prime numbers are coprime for all smaller numbers ] hash: 0000001590-0f1875ed242f480c0f53effa8d72de12c5abdaa758b6eee86675129afbed7a14 [Listed Érdi Gergő as a contributor. Nils Anders Danielsson **20120507160359 Ignore-this: 82f7bdc153d6e720a472a8557b8c2545 ] hash: 0000000727-c29abc428e68d2b908f6a53380d4495e6c62965bdffd6cccb1897720f7d165c1 [Adapted Gergő's patch to my taste. Nils Anders Danielsson **20120507160750 Ignore-this: 811c6d096fb79afe132b73bbbe7dbc60 ] hash: 0000003013-600f116c803d06dba03692e7925af3b76ef88bc37849ade0c8adcf12de6a0cdb [Replaced --no-termination-check with NO_TERMINATION_CHECK. Nils Anders Danielsson **20120418095116 Ignore-this: 77deeecfa1abe5aa590df671c913ac3 ] hash: 0000000300-68582d9e767d652223f3f629955671284c47e7cdb051696453e7cb2e2f6c7dad [Added i*j≡0⇒i≡0∨j≡0 to Data.Nat.Properties Joachim Breitner **20120510094133 Ignore-this: e7d50186d5a2a2c4246e21bdce7ab6bb This goes well with i+j≡0⇒i≡0 and i*j≡1⇒i≡1. ] hash: 0000000554-354634f3c3ea7eaa8f2447a047ce8ed36335ba5e6f7a206d23a4413515dbcc99 [Added toℕ-injective to Data.Fin.Props Joachim Breitner **20120510095237 Ignore-this: b1bf2333914f4fc13559ea732f5f25bd ] hash: 0000000524-edfe31882401841e33333b97933188ffc5e00641638906456443bf9062ba05f9 [Added i+[j∸m]≡i+j∸m to Data.Nat.Properties Joachim Breitner **20120510095820 Ignore-this: b438986ce991c51984487bd6b2ffc0ea Which goes well with lemmata like [i+j]∸[i+k]≡j∸k. ] hash: 0000000795-fac6f2332053141034bef32134920ff1f18a754451f7069a8d60af06f2ba4486 [Two lemmas about the monotonicity of ∸ Joachim Breitner **20120511091215 Ignore-this: 63c764bd45f4804dfe747a99a48f71e0 ] hash: 0000000709-2cda9173ef0c72567ffd0a39db999e9e87fe41f371447f384364388b6f14b1db [Added n∸n≡0. Renamed i+[j∸m]≡i+j∸m to +-∸-assoc. Nils Anders Danielsson **20120515142949 Ignore-this: f442f0811d5ce13f3bb127b6906a3781 ] hash: 0000002759-86daadab4130c23b93da7ee292a3ee588bfec4b908b881ef1451579df9f6a208 [Replaced ∸-mono₁ and ∸-mono₂ with ∸-mono. Nils Anders Danielsson **20120515143004 Ignore-this: eeb39c5ff560cd4f1979f98ae476c8d3 ] hash: 0000001125-feb500d2092a28dac7721289340c0afa338de90991730af76461e3d1933978b4 [Cosmetic changes. Nils Anders Danielsson **20120515143505 Ignore-this: 85998a1b0aa9ebbceb47a0f69adafac2 ] hash: 0000001631-b25472249e52b245d6635beea4a9760a1dc3d19653383679dabc11cadb59f77a [Removed the postulated quotients, which turned out to be unsound. Nils Anders Danielsson **20120516132746 Ignore-this: 59beea0edf033b56843cff95b9e5290 ] hash: 0000006671-4401d2501ae67f68685dbd0a281a05f88e3d598cf3b1283a5c7dd6742d4d4271 [Generalised Relation.Binary.List.Pointwise from Rel to REL. Stevan Andjelkovic **20120515184226 Ignore-this: 44eb5ba7562ddc445a86d3e3cecd6f94 ] hash: 0000012535-a660733608944ed65cc80ae514af766fd02d6c6991ff19e0b2c9afb11af725e2 [Cosmetic changes. Nils Anders Danielsson **20120516173847 Ignore-this: 77fdc80d47930231c701149a4e869d26 ] hash: 0000001583-7250727c4720e0af71fe5f9ef7778e22e0f826a976af8a6176b7258c5ec8fc8c [Listed Stevan Andjelkovic as a contributor. Nils Anders Danielsson **20120516174739 Ignore-this: 46edec47d470a1e882d5cc6d0cad76f1 ] hash: 0000001047-66b2eaf0cbf9efc26514fe49a842d6bb27f756250c60212e75735fbfda9e3bfe