{"push_id":919805657,"size":21,"distinct_size":2,"ref":"refs/heads/master","head":"bc2950a23768ab35ea853f0d5a44b92b29072b0b","before":"3fdd6da1c9ad27c965ec68a6a900e04a5c735241","commits":[{"sha":"1af1c8d3f48639a9ac19a1af922e6bbfab604c1b","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Work on making record fupd fns more polymorphic\n\nThis is github issue #173.\n\nSelftest checks for right behaviour.  But an earlier test is failing\nbecause the handling of \"big records\" hasn't been completely updated.","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/1af1c8d3f48639a9ac19a1af922e6bbfab604c1b"},{"sha":"c3cde98f9f9b1f156d0181752acae96189ce5c71","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Polish preterm API to remove unused parameter.\n\nmake_qconst didn't read/use its overload_info parameter, so there seems\nno point having that parameter in the API.","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/c3cde98f9f9b1f156d0181752acae96189ce5c71"},{"sha":"a16605e396892e4cb6a2af509d95e78d5c6ab118","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Fixes with polymorphic record literals\n\n1. When you write <| fld1 := foo ; fld2 := bar |> there is secretly an\n   ARB term hiding in the result.  You don't want that ARB term to be\n   unnecessarily polymorphic.\n\n2. TypeBase.mk_record has to adjust for the possibility that fupds can\n   have types of the form\n\n      fupd : (α fldty -> β fldty) -> (α,γ) rcd -> (β, γ) rcd\n\nContinuing work on github issue #173","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/a16605e396892e4cb6a2af509d95e78d5c6ab118"},{"sha":"dcde507a6da7b76c05cdbc5e67a9c1f2881ed144","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Fix proof of \"bigrec\" thms for polymorphic records\n\nThese are the theorems that are proved to knit together the view of the\nrecord that the user expects and the underlying reality, which is a\nrecord of records.  These are stated and proved after the various\nunderlying record types are defined.\n\nTests in src/datatype/selftest.sml\n\nThis is work on github issue #173","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/dcde507a6da7b76c05cdbc5e67a9c1f2881ed144"},{"sha":"9ca8abc51f0b35924382686397c211c80efe70a7","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Get EmitML to handle polymorphic records correctly\n\nTests in src/emit/theory_tests.\n\nCloses github issue #173","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/9ca8abc51f0b35924382686397c211c80efe70a7"},{"sha":"bb82b3fa54a1f6a975bc0ae6d62bc9091f264bf3","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Merge branch 'polyrcd' into k11-release-prep","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/bb82b3fa54a1f6a975bc0ae6d62bc9091f264bf3"},{"sha":"ea8d1b7b76e9e27dae16055b45adf19e137eff8b","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Record polyrcd update work in release notes\n\nRelated to issue #173","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/ea8d1b7b76e9e27dae16055b45adf19e137eff8b"},{"sha":"2e0240f45db8c72446647cafd8270dd9d36ac869","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Restore old chapter about tactics in DESCRIPTION\n\nI want to tidy this up and have it help address github issue #273, which\nis to document and encourage use of modern tactics.","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/2e0240f45db8c72446647cafd8270dd9d36ac869"},{"sha":"a5579a1ac7eaf95b133fbb5b0f57f47137f92881","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Get trailing-wspace deletion to look at more files\n\nNow it also looks in .bib and .doc files","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/a5579a1ac7eaf95b133fbb5b0f57f47137f92881"},{"sha":"5cef4bb81049cfa952a39f3ee3c5cbc7e232ad85","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Delete trailing whitespace in description.bib","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/5cef4bb81049cfa952a39f3ee3c5cbc7e232ad85"},{"sha":"e7f4d74ae2a60ed3d9c0afcff0d5497299786056","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Move lcsymtacs functions to natural homes\n\nFor example, we do not need to have >> in lcsymtacs; it might as be in\nTactical. The ultimate aim is to do away with lcsymtacs entirely.\n\nThis is work towards github issue #274","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/e7f4d74ae2a60ed3d9c0afcff0d5497299786056"},{"sha":"8f6d778428321e0acded942474409ab84427f732","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Delete trailing whitespace in help/Docfiles","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/8f6d778428321e0acded942474409ab84427f732"},{"sha":"eb991075af1551a435b4c3fcdcddcc64c87f949c","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Provide gentactic's type definition in Abbrev.sml","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/eb991075af1551a435b4c3fcdcddcc64c87f949c"},{"sha":"48bce6f2738ec5468cb42cf8e9e3b86331b4d23a","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Move some tactics from lcsymtacs to Tactic{,al}\n\nAs per Github issue #274","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/48bce6f2738ec5468cb42cf8e9e3b86331b4d23a"},{"sha":"5b282aae73695545142f27e98f98b2fa70af435b","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"More moving lcsymtacs implementations elsewhere\n\nEventually lcsymtacs will just be a bunch of 'open' declarations, and\nthen people won't bother to include it at all.","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/5b282aae73695545142f27e98f98b2fa70af435b"},{"sha":"39e206bcebcb1836f113a25450833d0726a37b71","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Adjusting DESCRIPTION's revived section on tactics","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/39e206bcebcb1836f113a25450833d0726a37b71"},{"sha":"8ef596ccc1a502b475260bcf4dec07126adb2f42","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"More hacking at Description's Tactics chapter","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/8ef596ccc1a502b475260bcf4dec07126adb2f42"},{"sha":"d0a11f5e940cbf8b5f82f53846da7b7af537931e","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Adjust installation instructions a little.\n\nFrom comments in github issue #324:\n* tell users not to use the --with-portable option when building Poly/ML\n* make it clear that the system installs \"in place\", and that once build\n  has done its thing, the system can't be moved.\n\nCloses #324","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/d0a11f5e940cbf8b5f82f53846da7b7af537931e"},{"sha":"ed8f0afe18bbc555585f804fc06e07b212bc0c9c","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"More work on Tactics chapter of Description","distinct":false,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/ed8f0afe18bbc555585f804fc06e07b212bc0c9c"},{"sha":"f8c23307c5e834512495859852b7d102b2152fbe","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Merged k11-release-prep into master","distinct":true,"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/commits/f8c23307c5e834512495859852b7d102b2152fbe"}]}