{"push_id":852021753,"size":17,"distinct_size":1,"ref":"refs/heads/monad","head":"c1e54399f761432c428964a6f7805843b8ad110e","before":"1eebf979a29e79296766b7a8331847ab70a2ab33","commits":[{"sha":"f9053c22028649f29395bc31d0a7afae982fac75","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Next release will be Kananaskis-11\n\nThis commit starts release preparation branch.","distinct":false,"url":"https://api.github.com/repos/jeremydaw/HOL/commits/f9053c22028649f29395bc31d0a7afae982fac75"},{"sha":"c1b43bda91b3c147d0f6528f5cf0ff80dec81903","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Tweak unicode-grep\n\n- more portable through use of character classes rather than Perl\n  regexps (backslashed characters inside [..])\n- allow presence of UOK on line with Unicode to suppress warning","distinct":false,"url":"https://api.github.com/repos/jeremydaw/HOL/commits/c1b43bda91b3c147d0f6528f5cf0ff80dec81903"},{"sha":"fda6dec35881742a7e750de74dc1c842d2ca4e14","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Clean src/ to remove Unicode (or to mark it as OK)\n\nMarking Unicode as OK is done by putting the UOK tag on the same line of\nthe relevant file.","distinct":false,"url":"https://api.github.com/repos/jeremydaw/HOL/commits/fda6dec35881742a7e750de74dc1c842d2ca4e14"},{"sha":"f03b6d2c2fe2fff0852a159a9bfe1b8cad0606aa","author":{"email":"dedfb5d35184997352c96c03dbc128840e913dd8@nicta.com.au","name":"Michael Norrish"},"message":"Improve Makefile for Developers' Manual","distinct":false,"url":"https://api.github.com/repos/jeremydaw/HOL/commits/f03b6d2c2fe2fff0852a159a9bfe1b8cad0606aa"},{"sha":"bd77b8fb0bb84711ac3cffc05b1ccdb77e4dc334","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Delete trailing whitespace","distinct":false,"url":"https://api.github.com/repos/jeremydaw/HOL/commits/bd77b8fb0bb84711ac3cffc05b1ccdb77e4dc334"},{"sha":"3a35ef493d1bca8fb0e28722e0da5da3968bf398","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Tidy unicode-grep; delete redundant find-nonascii","distinct":false,"url":"https://api.github.com/repos/jeremydaw/HOL/commits/3a35ef493d1bca8fb0e28722e0da5da3968bf398"},{"sha":"594f9a631b5e4bad652c6272867bc3d9f6e19a06","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Use regression tests to check for Unicode in src","distinct":false,"url":"https://api.github.com/repos/jeremydaw/HOL/commits/594f9a631b5e4bad652c6272867bc3d9f6e19a06"},{"sha":"c59b8cb17d30d3f911d7e8f8938b995f1527bd2e","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Tweak description of option theory's case constant\n\nIn particular, it's now called option_CASE and takes its arguments in a\ndifferent order.\n\nAlso fix a typographic fix (using \\tt in paragraph to refer to option\ntype rather than \\sf)","distinct":false,"url":"https://api.github.com/repos/jeremydaw/HOL/commits/c59b8cb17d30d3f911d7e8f8938b995f1527bd2e"},{"sha":"036c9844e404068ab9d4701b76df1743d4411c66","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Improve tactic selection/movement in emacs mode\n\nAlso add new \"execute the next tactic\" binding on M-h M-e, which\n\"automagically\" selects the next tactic from the source buffer, and\napplies it. If the next tactic is, say, a parenthesised argument to\n>-/THEN1, it will select all of it. To step into such a tactic, the\nuser has to manually move the cursor into the sexp.","distinct":false,"url":"https://api.github.com/repos/jeremydaw/HOL/commits/036c9844e404068ab9d4701b76df1743d4411c66"},{"sha":"11ce3a0b21fa430211a8eed20d9d7fac5e9a90c0","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Add \"termination goal\" to g/stack menu in hol-mode","distinct":false,"url":"https://api.github.com/repos/jeremydaw/HOL/commits/11ce3a0b21fa430211a8eed20d9d7fac5e9a90c0"},{"sha":"66b7f841006a034761545daa9e365d493e6b6dab","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Fix unescaped $ syntax error in doc-file.\n\nDollar signs have to occur between braces ({ .. }) so that LaTeX only\nsees them inside verbatim chunks.","distinct":false,"url":"https://api.github.com/repos/jeremydaw/HOL/commits/66b7f841006a034761545daa9e365d493e6b6dab"},{"sha":"4322c922954015baa59303a97787ccc050d41fc9","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Merge k11-release-prep into master\n\nThere's no reason to stop master picking up the \"good stuff\" from the\nrelease preparation branch. It will certainly be merged in again after\nthe release as well.","distinct":false,"url":"https://api.github.com/repos/jeremydaw/HOL/commits/4322c922954015baa59303a97787ccc050d41fc9"},{"sha":"923e92e2eb7fdc16f7bdd8e6bfc937aec12a8485","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"MATCH_ABBREV tactics now ignore _ in patterns\n\nTactics affected are\n- MATCH_ABBREV_TAC\n- HO_MATCH_ABBREV_TAC\n- MATCH_ASSUM_ABBREV_TAC\n\nDocumented and self-tested","distinct":false,"url":"https://api.github.com/repos/jeremydaw/HOL/commits/923e92e2eb7fdc16f7bdd8e6bfc937aec12a8485"},{"sha":"a813b78cb6986aec5f78fd4d7460a6055941e85b","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Delete trailing whitespace in arithmeticScript","distinct":false,"url":"https://api.github.com/repos/jeremydaw/HOL/commits/a813b78cb6986aec5f78fd4d7460a6055941e85b"},{"sha":"f04b11be6c4c2d6bd5f01ed22dccbbd8ed7a7557","author":{"email":"5b271689e2a5be36b59ea0b1716899fe80ad26c5@nicta.com.au","name":"Michael Norrish"},"message":"Remove Unicode under src/","distinct":false,"url":"https://api.github.com/repos/jeremydaw/HOL/commits/f04b11be6c4c2d6bd5f01ed22dccbbd8ed7a7557"},{"sha":"e256184a914b1ea889bfec7a72a27e394c03e8c9","author":{"email":"4e9e50b5d0f80819758cc85d7b06abc0007a7fde@member.fsf.org","name":"Ramana Kumar"},"message":"update my email address","distinct":false,"url":"https://api.github.com/repos/jeremydaw/HOL/commits/e256184a914b1ea889bfec7a72a27e394c03e8c9"},{"sha":"c1e54399f761432c428964a6f7805843b8ad110e","author":{"email":"b3f594e10a9edcf5413cf1190121d45078c62290@cecs.anu.edu.au","name":"Jeremy Dawson"},"message":"LINV_OPT, Left inverse, to option type\n\nresult is NONE outside image of domain\nalso new result CARD_IMAGE","distinct":true,"url":"https://api.github.com/repos/jeremydaw/HOL/commits/c1e54399f761432c428964a6f7805843b8ad110e"}]}