{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":353685,"defaultBranch":"develop","name":"HOL","ownerLogin":"HOL-Theorem-Prover","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2009-10-29T02:47:31.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/8379840?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1724238231.0","currentOid":""},"activityList":{"items":[{"before":"72a01e7935ee7175f22527332d54ac58085668ed","after":"e1640d96f40e98a9d5b7ad0907e652a0e665bcab","ref":"refs/heads/master","pushedAt":"2024-09-30T04:49:54.000Z","pushType":"push","commitsCount":7,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Prove a number of theorems about list$adjacent\n\nIncluding automatic rewrite\n\n  ⊢ adjacent (REVERSE xs) a b ⇔ adjacent xs b a","shortMessageHtmlLink":"Prove a number of theorems about list$adjacent"}},{"before":"c453c8ab2e1ea7e27f874c54d5dd810e22594f17","after":"202fecab35c4fbeecc8e77331d38acd15ff58fb9","ref":"refs/heads/develop","pushedAt":"2024-09-30T04:37:31.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Add some entries to DESCRIPTION's index","shortMessageHtmlLink":"Add some entries to DESCRIPTION's index"}},{"before":"8397f829220eaa7ae0a18ac26115fb430e79df13","after":"c453c8ab2e1ea7e27f874c54d5dd810e22594f17","ref":"refs/heads/develop","pushedAt":"2024-09-30T01:41:20.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Remove some HOL88 quoting from a .doc file","shortMessageHtmlLink":"Remove some HOL88 quoting from a .doc file"}},{"before":"e1640d96f40e98a9d5b7ad0907e652a0e665bcab","after":"8397f829220eaa7ae0a18ac26115fb430e79df13","ref":"refs/heads/develop","pushedAt":"2024-09-30T00:17:24.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Zero-terminated repl v2","shortMessageHtmlLink":"Zero-terminated repl v2"}},{"before":"938c94e16e0f838bd6822be1f5f04c7f5374931d","after":"e1640d96f40e98a9d5b7ad0907e652a0e665bcab","ref":"refs/heads/develop","pushedAt":"2024-09-27T00:51:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Prove a number of theorems about list$adjacent\n\nIncluding automatic rewrite\n\n  ⊢ adjacent (REVERSE xs) a b ⇔ adjacent xs b a","shortMessageHtmlLink":"Prove a number of theorems about list$adjacent"}},{"before":"2b7b84fd9d288977243e859794334723ffaf407a","after":"938c94e16e0f838bd6822be1f5f04c7f5374931d","ref":"refs/heads/develop","pushedAt":"2024-09-26T07:17:17.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Build real heap on top of core HOL heap (saving some time)","shortMessageHtmlLink":"Build real heap on top of core HOL heap (saving some time)"}},{"before":"19ebd252661532b54e87ded3aeddf0ea73874a2f","after":"2b7b84fd9d288977243e859794334723ffaf407a","ref":"refs/heads/develop","pushedAt":"2024-09-26T01:49:05.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"more context lines on failure","shortMessageHtmlLink":"more context lines on failure"}},{"before":"7bf55e0eb37d0d68268a5b6c2d55dc2895fd6361","after":"72a01e7935ee7175f22527332d54ac58085668ed","ref":"refs/heads/master","pushedAt":"2024-09-25T04:28:26.000Z","pushType":"push","commitsCount":14,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Add more primitive proof rules","shortMessageHtmlLink":"Add more primitive proof rules"}},{"before":"72a01e7935ee7175f22527332d54ac58085668ed","after":"19ebd252661532b54e87ded3aeddf0ea73874a2f","ref":"refs/heads/develop","pushedAt":"2024-09-25T02:05:52.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"add an extra 0 for initial prompt","shortMessageHtmlLink":"add an extra 0 for initial prompt"}},{"before":"04bef39b14ed85479d1ff06227ae84da34f01950","after":"72a01e7935ee7175f22527332d54ac58085668ed","ref":"refs/heads/develop","pushedAt":"2024-09-23T23:08:36.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Add more primitive proof rules","shortMessageHtmlLink":"Add more primitive proof rules"}},{"before":"c7ca76229deddf769c065c798756de5369e673c9","after":"04bef39b14ed85479d1ff06227ae84da34f01950","ref":"refs/heads/develop","pushedAt":"2024-09-23T05:13:28.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Fix errors caused by generated names","shortMessageHtmlLink":"Fix errors caused by generated names"}},{"before":"859de11397e52a32678524d1df1f320389d31653","after":"c7ca76229deddf769c065c798756de5369e673c9","ref":"refs/heads/develop","pushedAt":"2024-09-23T00:24:40.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Remove pauses in configure script","shortMessageHtmlLink":"Remove pauses in configure script"}},{"before":"0ee93686c4a5eaea3309ddf75e7744d9c3e87734","after":"859de11397e52a32678524d1df1f320389d31653","ref":"refs/heads/develop","pushedAt":"2024-09-23T00:24:01.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Fixes to opentheory build","shortMessageHtmlLink":"Fixes to opentheory build"}},{"before":"809419914cc3655e2ed41435f7dd3ebd6dedade1","after":"0ee93686c4a5eaea3309ddf75e7744d9c3e87734","ref":"refs/heads/develop","pushedAt":"2024-09-23T00:22:58.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Fixed some obvious issues in Emacs related files","shortMessageHtmlLink":"Fixed some obvious issues in Emacs related files"}},{"before":"9043f61db606489f5498a0940f07e2383a97289c","after":"809419914cc3655e2ed41435f7dd3ebd6dedade1","ref":"refs/heads/develop","pushedAt":"2024-09-23T00:21:17.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Report error locations on unhandled exceptions","shortMessageHtmlLink":"Report error locations on unhandled exceptions"}},{"before":"d683671b07c27a65aebc32e1188cb245cedeb532","after":"9043f61db606489f5498a0940f07e2383a97289c","ref":"refs/heads/develop","pushedAt":"2024-09-13T01:04:30.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Add definition of r-partite graphs and in particular bipartite graphs (#1299)\n\n* [fsgraph] Add definition of r-partite graphs and in particular bipartite graphs\r\n\r\n* removed trailing whitespaces...\r\n\r\n* Modified definitions by moving partitions to existence","shortMessageHtmlLink":"Add definition of r-partite graphs and in particular bipartite graphs (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2518290622\" data-permission-text=\"Title is private\" data-url=\"https://github.com/HOL-Theorem-Prover/HOL/issues/1299\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/HOL-Theorem-Prover/HOL/pull/1299/hovercard\" href=\"https://github.com/HOL-Theorem-Prover/HOL/pull/1299\">…</a>"}},{"before":"be2d4f0e21ddb0858e98e72607788ce5261b6ce0","after":"d683671b07c27a65aebc32e1188cb245cedeb532","ref":"refs/heads/develop","pushedAt":"2024-09-11T23:27:47.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Document DB.find better, given ec5eda5de6164a and following commits","shortMessageHtmlLink":"Document DB.find better, given <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/HOL-Theorem-Prover/HOL/commit/ec5eda5de6164a5420d9565136e5eca7492ea635/hovercard\" href=\"https://github.com/HOL-Theorem-Prover/HOL/commit/ec5eda5de6164a5420d9565136e5eca7492ea635\"><tt>ec5eda5</tt></a> and following commits"}},{"before":"14b4197fb0dd7210dfe684a9533b0e3ac853a238","after":"be2d4f0e21ddb0858e98e72607788ce5261b6ce0","ref":"refs/heads/develop","pushedAt":"2024-09-11T00:43:17.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"konrad-slind","name":"Konrad Slind","path":"/konrad-slind","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1105935?s=80&v=4"},"commit":{"message":"Fix typo.","shortMessageHtmlLink":"Fix typo."}},{"before":"7bf55e0eb37d0d68268a5b6c2d55dc2895fd6361","after":"14b4197fb0dd7210dfe684a9533b0e3ac853a238","ref":"refs/heads/develop","pushedAt":"2024-09-10T06:42:27.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Simplified code with prob_div_mul_refl lemma (#1298)\n\n* Simplified code with prob_div_mul_refl lemma\r\n\r\n* Replace MATCH_MP_TAC by simp[prob_div_mul_refl]","shortMessageHtmlLink":"Simplified code with prob_div_mul_refl lemma (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2506831625\" data-permission-text=\"Title is private\" data-url=\"https://github.com/HOL-Theorem-Prover/HOL/issues/1298\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/HOL-Theorem-Prover/HOL/pull/1298/hovercard\" href=\"https://github.com/HOL-Theorem-Prover/HOL/pull/1298\">#1298</a>)"}},{"before":"ba3052854752b85c309b047ba1e544f17084e071","after":"7bf55e0eb37d0d68268a5b6c2d55dc2895fd6361","ref":"refs/heads/master","pushedAt":"2024-09-10T04:08:33.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Fix bug in reduceLib.NOT_CONV\n\nThanks to someplaceguy for bug report.","shortMessageHtmlLink":"Fix bug in reduceLib.NOT_CONV"}},{"before":"3f726a4243be5a37ebd3437ceeab9bbafdcb6139","after":"7bf55e0eb37d0d68268a5b6c2d55dc2895fd6361","ref":"refs/heads/develop","pushedAt":"2024-09-09T04:53:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Fix bug in reduceLib.NOT_CONV\n\nThanks to someplaceguy for bug report.","shortMessageHtmlLink":"Fix bug in reduceLib.NOT_CONV"}},{"before":"0027639d9586b620303c54f45954b93896dd4587","after":"ba3052854752b85c309b047ba1e544f17084e071","ref":"refs/heads/master","pushedAt":"2024-09-09T04:05:02.000Z","pushType":"push","commitsCount":11,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Add lemma prob_div_mul_relf, refactor code in proofs of BAYES_THEOREM, and COND_PROB_ADDITIVE (#1293)\n\n* Add lemma prob_div_mul_relf, refactor code, including BAYES_THEOREM, and COND_PROB_ADDITIVE\r\n\r\n* Replace Unicode characters\r\n\r\n* remove set up of Holscript mode","shortMessageHtmlLink":"Add lemma prob_div_mul_relf, refactor code in proofs of BAYES_THEOREM…"}},{"before":"0f9ee5c92920aa43012234488972292395d373dc","after":"3f726a4243be5a37ebd3437ceeab9bbafdcb6139","ref":"refs/heads/develop","pushedAt":"2024-09-09T01:10:33.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Updates to convergence concepts for potential infinite-valued r.v.'s (#1295)\n\n* Updates to convergence concepts for potential infinite-valued r.v.'s\r\n\r\n* Remove unfinished work...\r\n\r\n* FTBFS\r\n\r\n* Added missing NUM_FLOOR_POS, etc. in realTheory\r\n\r\n* FTBFS examples/dependability","shortMessageHtmlLink":"Updates to convergence concepts for potential infinite-valued r.v.'s (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2499857585\" data-permission-text=\"Title is private\" data-url=\"https://github.com/HOL-Theorem-Prover/HOL/issues/1295\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/HOL-Theorem-Prover/HOL/pull/1295/hovercard\" href=\"https://github.com/HOL-Theorem-Prover/HOL/pull/1295\">#…</a>"}},{"before":"ba3052854752b85c309b047ba1e544f17084e071","after":"0f9ee5c92920aa43012234488972292395d373dc","ref":"refs/heads/develop","pushedAt":"2024-09-09T01:06:32.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Fix bug in L3 spec of RISC-V (JAL and JALR addr alignment)","shortMessageHtmlLink":"Fix bug in L3 spec of RISC-V (JAL and JALR addr alignment)"}},{"before":"4277a75e45fddd77e02c390c8d347b24592f4841","after":"ba3052854752b85c309b047ba1e544f17084e071","ref":"refs/heads/develop","pushedAt":"2024-09-03T23:00:37.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Add lemma prob_div_mul_relf, refactor code in proofs of BAYES_THEOREM, and COND_PROB_ADDITIVE (#1293)\n\n* Add lemma prob_div_mul_relf, refactor code, including BAYES_THEOREM, and COND_PROB_ADDITIVE\r\n\r\n* Replace Unicode characters\r\n\r\n* remove set up of Holscript mode","shortMessageHtmlLink":"Add lemma prob_div_mul_relf, refactor code in proofs of BAYES_THEOREM…"}},{"before":"9e00c4ce6fbc07a18d373d48d2aae2f296dbfe89","after":"4277a75e45fddd77e02c390c8d347b24592f4841","ref":"refs/heads/develop","pushedAt":"2024-09-03T08:31:14.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Handle schematic inductive definitions better\n\nCloses #1296","shortMessageHtmlLink":"Handle schematic inductive definitions better"}},{"before":"ec4a75e0e390ced38f833ea0bf0b90f8cd66073d","after":"9e00c4ce6fbc07a18d373d48d2aae2f296dbfe89","ref":"refs/heads/develop","pushedAt":"2024-09-03T00:58:18.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Modernise some syntax","shortMessageHtmlLink":"Modernise some syntax"}},{"before":"3cb0aba4cedc178295854e32fa5081b3394d5249","after":"ec4a75e0e390ced38f833ea0bf0b90f8cd66073d","ref":"refs/heads/develop","pushedAt":"2024-09-02T02:29:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Document unicode-grep in Developers' manual","shortMessageHtmlLink":"Document unicode-grep in Developers' manual"}},{"before":"0b23319c8ecc906f21d2a366c025d7a6594ee2ea","after":"3cb0aba4cedc178295854e32fa5081b3394d5249","ref":"refs/heads/develop","pushedAt":"2024-09-02T02:19:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Minor additions to developers manual.","shortMessageHtmlLink":"Minor additions to developers manual."}},{"before":"0619699bbfe8a41cae9cf23afe8ca39c42aae11f","after":"0b23319c8ecc906f21d2a366c025d7a6594ee2ea","ref":"refs/heads/develop","pushedAt":"2024-09-02T01:59:30.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mn200","name":"Michael Norrish","path":"/mn200","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/145647?s=80&v=4"},"commit":{"message":"Document source code requirements in the Developers' manual","shortMessageHtmlLink":"Document source code requirements in the Developers' manual"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0zMFQwNDo0OTo1NC4wMDAwMDBazwAAAATEQlRN","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0wMlQwMTo1OTozMC4wMDAwMDBazwAAAASqHrPz"}},"title":"Activity · HOL-Theorem-Prover/HOL"}