You can subscribe to this list here.
2001 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
(21) |
Sep
(54) |
Oct
(196) |
Nov
(158) |
Dec
(139) |
---|---|---|---|---|---|---|---|---|---|---|---|---|
2002 |
Jan
(62) |
Feb
(98) |
Mar
(42) |
Apr
(137) |
May
(141) |
Jun
(108) |
Jul
(70) |
Aug
(117) |
Sep
(106) |
Oct
(25) |
Nov
(34) |
Dec
(27) |
2003 |
Jan
(53) |
Feb
(53) |
Mar
(102) |
Apr
(62) |
May
(10) |
Jun
(77) |
Jul
(83) |
Aug
(72) |
Sep
(74) |
Oct
(118) |
Nov
(6) |
Dec
(6) |
2004 |
Jan
(89) |
Feb
(43) |
Mar
(41) |
Apr
(20) |
May
(30) |
Jun
(60) |
Jul
(204) |
Aug
(79) |
Sep
(19) |
Oct
(37) |
Nov
(25) |
Dec
(34) |
2005 |
Jan
(174) |
Feb
(107) |
Mar
(48) |
Apr
(70) |
May
(35) |
Jun
(115) |
Jul
(257) |
Aug
(63) |
Sep
(62) |
Oct
(51) |
Nov
(68) |
Dec
(47) |
2006 |
Jan
(50) |
Feb
(129) |
Mar
(73) |
Apr
(13) |
May
(91) |
Jun
(135) |
Jul
(104) |
Aug
(117) |
Sep
(151) |
Oct
(101) |
Nov
(69) |
Dec
(51) |
2007 |
Jan
(68) |
Feb
(45) |
Mar
(44) |
Apr
(21) |
May
(40) |
Jun
(27) |
Jul
(76) |
Aug
(29) |
Sep
(12) |
Oct
(61) |
Nov
(32) |
Dec
(16) |
2008 |
Jan
(35) |
Feb
(26) |
Mar
(46) |
Apr
(79) |
May
(61) |
Jun
(38) |
Jul
(58) |
Aug
(64) |
Sep
(96) |
Oct
(86) |
Nov
(66) |
Dec
(80) |
2009 |
Jan
(53) |
Feb
(81) |
Mar
(104) |
Apr
(68) |
May
(61) |
Jun
(78) |
Jul
(138) |
Aug
(74) |
Sep
(157) |
Oct
(132) |
Nov
(113) |
Dec
(78) |
2010 |
Jan
(129) |
Feb
(101) |
Mar
(146) |
Apr
(158) |
May
(85) |
Jun
(98) |
Jul
(80) |
Aug
(124) |
Sep
(123) |
Oct
(98) |
Nov
(37) |
Dec
(51) |
2011 |
Jan
(82) |
Feb
(36) |
Mar
(50) |
Apr
(50) |
May
(52) |
Jun
(62) |
Jul
(33) |
Aug
(61) |
Sep
(125) |
Oct
(63) |
Nov
(14) |
Dec
(17) |
2012 |
Jan
(22) |
Feb
(36) |
Mar
(177) |
Apr
(77) |
May
(60) |
Jun
(46) |
Jul
(127) |
Aug
(96) |
Sep
(58) |
Oct
(72) |
Nov
(40) |
Dec
(44) |
2013 |
Jan
(42) |
Feb
(42) |
Mar
(5) |
Apr
(24) |
May
(38) |
Jun
(25) |
Jul
(36) |
Aug
(35) |
Sep
(9) |
Oct
(29) |
Nov
(60) |
Dec
(24) |
2014 |
Jan
(26) |
Feb
(32) |
Mar
(28) |
Apr
(28) |
May
(35) |
Jun
(34) |
Jul
(23) |
Aug
(37) |
Sep
(28) |
Oct
(33) |
Nov
(38) |
Dec
(24) |
2015 |
Jan
(36) |
Feb
(38) |
Mar
(54) |
Apr
(4) |
May
(16) |
Jun
(21) |
Jul
(25) |
Aug
(65) |
Sep
(54) |
Oct
(63) |
Nov
(60) |
Dec
(35) |
2016 |
Jan
(106) |
Feb
(35) |
Mar
(93) |
Apr
(65) |
May
(45) |
Jun
(48) |
Jul
(44) |
Aug
(65) |
Sep
(48) |
Oct
(31) |
Nov
(63) |
Dec
(33) |
2017 |
Jan
(46) |
Feb
(48) |
Mar
(36) |
Apr
(38) |
May
(39) |
Jun
(65) |
Jul
(49) |
Aug
(48) |
Sep
(52) |
Oct
(86) |
Nov
(31) |
Dec
(22) |
2018 |
Jan
(60) |
Feb
(21) |
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
2019 |
Jan
(29) |
Feb
(122) |
Mar
(112) |
Apr
(60) |
May
(141) |
Jun
(75) |
Jul
(83) |
Aug
(73) |
Sep
(48) |
Oct
(67) |
Nov
(124) |
Dec
(34) |
2020 |
Jan
(115) |
Feb
(138) |
Mar
(63) |
Apr
(26) |
May
(102) |
Jun
(85) |
Jul
(51) |
Aug
(106) |
Sep
(44) |
Oct
(43) |
Nov
(40) |
Dec
(82) |
2021 |
Jan
(75) |
Feb
(35) |
Mar
(65) |
Apr
(11) |
May
(79) |
Jun
(48) |
Jul
(41) |
Aug
(66) |
Sep
(45) |
Oct
(55) |
Nov
(88) |
Dec
(50) |
2022 |
Jan
(67) |
Feb
(51) |
Mar
(43) |
Apr
(37) |
May
(26) |
Jun
(25) |
Jul
(16) |
Aug
(26) |
Sep
(24) |
Oct
(24) |
Nov
(16) |
Dec
(23) |
2023 |
Jan
(32) |
Feb
(8) |
Mar
(6) |
Apr
(6) |
May
(22) |
Jun
(42) |
Jul
(52) |
Aug
(45) |
Sep
(29) |
Oct
(30) |
Nov
(40) |
Dec
(24) |
2024 |
Jan
(67) |
Feb
(40) |
Mar
(33) |
Apr
(47) |
May
(50) |
Jun
(46) |
Jul
(41) |
Aug
(41) |
Sep
(24) |
Oct
|
Nov
|
Dec
|
From: Mario C. <no...@gi...> - 2024-09-23 23:09:04
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 72a01e7935ee7175f22527332d54ac58085668ed https://github.com/HOL-Theorem-Prover/HOL/commit/72a01e7935ee7175f22527332d54ac58085668ed Author: Mario Carneiro <di...@gm...> Date: 2024-09-24 (Tue, 24 Sep 2024) Changed paths: M .gitignore M src/opentheory/postbool/Logging.sml M src/thm/otknl-thm.ML M src/thm/otknl-thmsig.ML Log Message: ----------- Add more primitive proof rules To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Michael N. <no...@gi...> - 2024-09-23 05:13:56
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: ad4d74db01c035f33683b62897d8f27fa5c58b92 https://github.com/HOL-Theorem-Prover/HOL/commit/ad4d74db01c035f33683b62897d8f27fa5c58b92 Author: Michael Norrish <mic...@an...> Date: 2024-09-23 (Mon, 23 Sep 2024) Changed paths: M src/marker/markerLib.sml M src/marker/markerScript.sml Log Message: ----------- Add constants to control simplifier selection of assumptions Commit: 04bef39b14ed85479d1ff06227ae84da34f01950 https://github.com/HOL-Theorem-Prover/HOL/commit/04bef39b14ed85479d1ff06227ae84da34f01950 Author: Michael Norrish <mic...@an...> Date: 2024-09-23 (Mon, 23 Sep 2024) Changed paths: M examples/formal-languages/regular/regularScript.sml Log Message: ----------- Fix errors caused by generated names Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/c7ca76229ded...04bef39b14ed To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Mario C. <no...@gi...> - 2024-09-23 00:25:08
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: c7ca76229deddf769c065c798756de5369e673c9 https://github.com/HOL-Theorem-Prover/HOL/commit/c7ca76229deddf769c065c798756de5369e673c9 Author: Mario Carneiro <di...@gm...> Date: 2024-09-23 (Mon, 23 Sep 2024) Changed paths: M tools-poly/smart-configure.sml Log Message: ----------- Remove pauses in configure script To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Mario C. <no...@gi...> - 2024-09-23 00:24:33
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 859de11397e52a32678524d1df1f320389d31653 https://github.com/HOL-Theorem-Prover/HOL/commit/859de11397e52a32678524d1df1f320389d31653 Author: Mario Carneiro <di...@gm...> Date: 2024-09-23 (Mon, 23 Sep 2024) Changed paths: A src/ring/src/EVAL_canonical.otd M src/ring/src/Holmakefile R src/ring/src/canonical.otd Log Message: ----------- Fixes to opentheory build To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Chun T. <no...@gi...> - 2024-09-23 00:23:25
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 0ee93686c4a5eaea3309ddf75e7744d9c3e87734 https://github.com/HOL-Theorem-Prover/HOL/commit/0ee93686c4a5eaea3309ddf75e7744d9c3e87734 Author: Chun Tian (binghe) <bin...@gm...> Date: 2024-09-23 (Mon, 23 Sep 2024) Changed paths: M tools/hol-input.el M tools/holscript-mode.el Log Message: ----------- Fixed some obvious issues in Emacs related files To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Mario C. <no...@gi...> - 2024-09-23 00:21:44
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 809419914cc3655e2ed41435f7dd3ebd6dedade1 https://github.com/HOL-Theorem-Prover/HOL/commit/809419914cc3655e2ed41435f7dd3ebd6dedade1 Author: Mario Carneiro <di...@gm...> Date: 2024-09-23 (Mon, 23 Sep 2024) Changed paths: M tools-poly/buildheap.ML M tools-poly/poly/poly-init2.ML Log Message: ----------- Report error locations on unhandled exceptions To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Chun T. <no...@gi...> - 2024-09-13 01:05:03
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 9043f61db606489f5498a0940f07e2383a97289c https://github.com/HOL-Theorem-Prover/HOL/commit/9043f61db606489f5498a0940f07e2383a97289c Author: Chun Tian <bin...@gm...> Date: 2024-09-13 (Fri, 13 Sep 2024) Changed paths: M examples/generic_graphs/fsgraphScript.sml Log Message: ----------- Add definition of r-partite graphs and in particular bipartite graphs (#1299) * [fsgraph] Add definition of r-partite graphs and in particular bipartite graphs * removed trailing whitespaces... * Modified definitions by moving partitions to existence To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Michael N. <no...@gi...> - 2024-09-11 23:28:19
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: d683671b07c27a65aebc32e1188cb245cedeb532 https://github.com/HOL-Theorem-Prover/HOL/commit/d683671b07c27a65aebc32e1188cb245cedeb532 Author: Michael Norrish <mic...@an...> Date: 2024-09-12 (Thu, 12 Sep 2024) Changed paths: M Manual/Interaction-emacs/interaction-emacs.stex M help/Docfiles/DB.find.doc Log Message: ----------- Document DB.find better, given ec5eda5de6164a and following commits To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Konrad S. <no...@gi...> - 2024-09-11 00:43:49
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 7b95ec6395bcd37477ad1010739dd824ca449c7f https://github.com/HOL-Theorem-Prover/HOL/commit/7b95ec6395bcd37477ad1010739dd824ca449c7f Author: Konrad Slind <kon...@gm...> Date: 2024-09-10 (Tue, 10 Sep 2024) Changed paths: M examples/formal-languages/FormalLangScript.sml M examples/formal-languages/regular/regexp2dfa.sml A examples/formal-languages/regular/regularScript.sml Log Message: ----------- NFA_LAGS = DFA_LANGS via subset construction Commit: 246518f494883264d1fb0fa036c040fb0fa2894a https://github.com/HOL-Theorem-Prover/HOL/commit/246518f494883264d1fb0fa036c040fb0fa2894a Author: Konrad Slind <kon...@gm...> Date: 2024-09-10 (Tue, 10 Sep 2024) Changed paths: M examples/formal-languages/FormalLangScript.sml M examples/formal-languages/regular/regularScript.sml Log Message: ----------- Progress on basic automata theory: - definition of REGULAR now makes the alphabet of the language explicit. - closure under complement, union, intersection, concatenation, and Kleene star. Commit: a71d31ed914ebfd1450da5b114a5254b8d979ec1 https://github.com/HOL-Theorem-Prover/HOL/commit/a71d31ed914ebfd1450da5b114a5254b8d979ec1 Author: Konrad Slind <kon...@gm...> Date: 2024-09-10 (Tue, 10 Sep 2024) Changed paths: M examples/formal-languages/FormalLangScript.sml M examples/formal-languages/regular/regularScript.sml Log Message: ----------- Get parsing/printing of \varepsilon symbol to (a) work and (b) be local. Commit: be2d4f0e21ddb0858e98e72607788ce5261b6ce0 https://github.com/HOL-Theorem-Prover/HOL/commit/be2d4f0e21ddb0858e98e72607788ce5261b6ce0 Author: Konrad Slind <kon...@gm...> Date: 2024-09-10 (Tue, 10 Sep 2024) Changed paths: M examples/formal-languages/regular/regexp2dfa.sml Log Message: ----------- Fix typo. Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/14b4197fb0dd...be2d4f0e21dd To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Tu P. <no...@gi...> - 2024-09-10 06:42:54
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 14b4197fb0dd7210dfe684a9533b0e3ac853a238 https://github.com/HOL-Theorem-Prover/HOL/commit/14b4197fb0dd7210dfe684a9533b0e3ac853a238 Author: Tu Phan <842...@us...> Date: 2024-09-10 (Tue, 10 Sep 2024) Changed paths: M src/probability/probabilityScript.sml Log Message: ----------- Simplified code with prob_div_mul_refl lemma (#1298) * Simplified code with prob_div_mul_refl lemma * Replace MATCH_MP_TAC by simp[prob_div_mul_refl] To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Michael N. <no...@gi...> - 2024-09-10 04:09:05
|
Branch: refs/heads/master Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 0f9ee5c92920aa43012234488972292395d373dc https://github.com/HOL-Theorem-Prover/HOL/commit/0f9ee5c92920aa43012234488972292395d373dc Author: Andreas Lindner <an...@kt...> Date: 2024-09-09 (Mon, 09 Sep 2024) Changed paths: M examples/l3-machine-code/riscv/src/riscv.spec Log Message: ----------- Fix bug in L3 spec of RISC-V (JAL and JALR addr alignment) Commit: 3f726a4243be5a37ebd3437ceeab9bbafdcb6139 https://github.com/HOL-Theorem-Prover/HOL/commit/3f726a4243be5a37ebd3437ceeab9bbafdcb6139 Author: Chun Tian <bin...@gm...> Date: 2024-09-09 (Mon, 09 Sep 2024) Changed paths: M examples/dependability/AvailabilityScript.sml M examples/dependability/case_studies/WSNScript.sml M examples/dependability/case_studies/smart_gridScript.sml M examples/probability/large_numberScript.sml M src/num/theories/whileScript.sml M src/pred_set/src/more_theories/topologyScript.sml M src/probability/extrealScript.sml M src/probability/martingaleScript.sml M src/probability/probabilityScript.sml M src/real/analysis/derivativeScript.sml M src/real/analysis/integrationScript.sml M src/real/analysis/limScript.sml M src/real/analysis/real_topologyScript.sml M src/real/analysis/seqScript.sml M src/real/metricScript.sml M src/real/netsScript.sml M src/real/realScript.sml Log Message: ----------- Updates to convergence concepts for potential infinite-valued r.v.'s (#1295) * Updates to convergence concepts for potential infinite-valued r.v.'s * Remove unfinished work... * FTBFS * Added missing NUM_FLOOR_POS, etc. in realTheory * FTBFS examples/dependability Commit: 7bf55e0eb37d0d68268a5b6c2d55dc2895fd6361 https://github.com/HOL-Theorem-Prover/HOL/commit/7bf55e0eb37d0d68268a5b6c2d55dc2895fd6361 Author: Michael Norrish <mic...@an...> Date: 2024-09-09 (Mon, 09 Sep 2024) Changed paths: M src/num/reduce/src/Boolconv.sml M src/num/reduce/src/selftest.sml Log Message: ----------- Fix bug in reduceLib.NOT_CONV Thanks to someplaceguy for bug report. Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/ba3052854752...7bf55e0eb37d To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Michael N. <no...@gi...> - 2024-09-09 04:54:13
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 7bf55e0eb37d0d68268a5b6c2d55dc2895fd6361 https://github.com/HOL-Theorem-Prover/HOL/commit/7bf55e0eb37d0d68268a5b6c2d55dc2895fd6361 Author: Michael Norrish <mic...@an...> Date: 2024-09-09 (Mon, 09 Sep 2024) Changed paths: M src/num/reduce/src/Boolconv.sml M src/num/reduce/src/selftest.sml Log Message: ----------- Fix bug in reduceLib.NOT_CONV Thanks to someplaceguy for bug report. To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Tu P. <no...@gi...> - 2024-09-09 04:05:31
|
Branch: refs/heads/master Home: https://github.com/HOL-Theorem-Prover/HOL Commit: bfe9f788ddcd0cee9e70b1d672160f01ff10ab00 https://github.com/HOL-Theorem-Prover/HOL/commit/bfe9f788ddcd0cee9e70b1d672160f01ff10ab00 Author: gengarrrr <104...@us...> Date: 2024-09-02 (Mon, 02 Sep 2024) Changed paths: M examples/Crypto/DES/des_propScript.sml Log Message: ----------- Update des_propScript.sml Commit: 6b42bd1b3a874b4ff6e94f45a6082300742bc1a7 https://github.com/HOL-Theorem-Prover/HOL/commit/6b42bd1b3a874b4ff6e94f45a6082300742bc1a7 Author: Chun Tian <bin...@gm...> Date: 2024-09-02 (Mon, 02 Sep 2024) Changed paths: M examples/probability/stochastic_processScript.sml M src/probability/borelScript.sml M src/probability/probabilityScript.sml M src/probability/sigma_algebraScript.sml Log Message: ----------- Infinite-dimensional Borel space Commit: d77fa087cdf0dd5088735107607e79ebeaadbe84 https://github.com/HOL-Theorem-Prover/HOL/commit/d77fa087cdf0dd5088735107607e79ebeaadbe84 Author: Chun Tian <bin...@gm...> Date: 2024-09-02 (Mon, 02 Sep 2024) Changed paths: M examples/CCS/CongruenceScript.sml M examples/CCS/ExampleScript.sml M examples/CCS/selftest.sml M examples/lambda/Holmakefile M examples/lambda/barendregt/boehmScript.sml M examples/lambda/barendregt/chap3Script.sml M examples/lambda/barendregt/finite_developmentsScript.sml M examples/lambda/barendregt/head_reductionScript.sml M examples/lambda/barendregt/normal_orderScript.sml M examples/lambda/barendregt/solvableScript.sml M examples/lambda/barendregt/standardisationScript.sml M examples/lambda/basics/Holmakefile M examples/lambda/basics/appFOLDLScript.sml M examples/lambda/basics/basic_swapScript.sml M examples/lambda/basics/generic_termsScript.sml M examples/lambda/basics/nomdatatype.sml M examples/lambda/basics/nomsetScript.sml M examples/lambda/basics/termScript.sml R examples/lambda/completeness/Holmakefile M src/list/src/listRangeScript.sml M src/list/src/listScript.sml M src/list/src/rich_listScript.sml M src/string/stringScript.sml Log Message: ----------- [lambda] Rank-based fresh name allocations; stage work on boehmTheory Commit: 0619699bbfe8a41cae9cf23afe8ca39c42aae11f https://github.com/HOL-Theorem-Prover/HOL/commit/0619699bbfe8a41cae9cf23afe8ca39c42aae11f Author: Chun Tian <bin...@gm...> Date: 2024-09-02 (Mon, 02 Sep 2024) Changed paths: M examples/lambda/barendregt/boehmScript.sml Log Message: ----------- Removed wrongly committed dead code Commit: 0b23319c8ecc906f21d2a366c025d7a6594ee2ea https://github.com/HOL-Theorem-Prover/HOL/commit/0b23319c8ecc906f21d2a366c025d7a6594ee2ea Author: Michael Norrish <mic...@an...> Date: 2024-09-02 (Mon, 02 Sep 2024) Changed paths: M Manual/Developers/developers.md Log Message: ----------- Document source code requirements in the Developers' manual Commit: 3cb0aba4cedc178295854e32fa5081b3394d5249 https://github.com/HOL-Theorem-Prover/HOL/commit/3cb0aba4cedc178295854e32fa5081b3394d5249 Author: Michael Norrish <mic...@an...> Date: 2024-09-02 (Mon, 02 Sep 2024) Changed paths: M Manual/Developers/developers.md Log Message: ----------- Minor additions to developers manual. Commit: ec4a75e0e390ced38f833ea0bf0b90f8cd66073d https://github.com/HOL-Theorem-Prover/HOL/commit/ec4a75e0e390ced38f833ea0bf0b90f8cd66073d Author: Michael Norrish <mic...@an...> Date: 2024-09-02 (Mon, 02 Sep 2024) Changed paths: M Manual/Developers/developers.md Log Message: ----------- Document unicode-grep in Developers' manual Commit: 2a72a369a2fafdbbabd97b0dc399a84e0a6fb59f https://github.com/HOL-Theorem-Prover/HOL/commit/2a72a369a2fafdbbabd97b0dc399a84e0a6fb59f Author: Michael Norrish <mic...@an...> Date: 2024-09-03 (Tue, 03 Sep 2024) Changed paths: M examples/lambda/basics/basic_swapScript.sml Log Message: ----------- Fix regression by removing unnecessary dependency on cardinalTheory The presence of cardinalTheory as an ancestor of lambda/basics/basic_swap caused a later definition that referred to ≼ to imagine that symbol referred to cardinalTheory's cardleq constant rather than listTheory's isPREFIX. Commit: 9e00c4ce6fbc07a18d373d48d2aae2f296dbfe89 https://github.com/HOL-Theorem-Prover/HOL/commit/9e00c4ce6fbc07a18d373d48d2aae2f296dbfe89 Author: Michael Norrish <mic...@an...> Date: 2024-09-03 (Tue, 03 Sep 2024) Changed paths: M examples/computability/kolmog/boolListsScript.sml Log Message: ----------- Modernise some syntax Commit: 4277a75e45fddd77e02c390c8d347b24592f4841 https://github.com/HOL-Theorem-Prover/HOL/commit/4277a75e45fddd77e02c390c8d347b24592f4841 Author: Michael Norrish <mic...@an...> Date: 2024-09-03 (Tue, 03 Sep 2024) Changed paths: M src/IndDef/InductiveDefinition.sml M src/IndDef/selftest.sml Log Message: ----------- Handle schematic inductive definitions better Closes #1296 Commit: ba3052854752b85c309b047ba1e544f17084e071 https://github.com/HOL-Theorem-Prover/HOL/commit/ba3052854752b85c309b047ba1e544f17084e071 Author: Tu Phan <842...@us...> Date: 2024-09-04 (Wed, 04 Sep 2024) Changed paths: M src/probability/probabilityScript.sml Log Message: ----------- Add lemma prob_div_mul_relf, refactor code in proofs of BAYES_THEOREM, and COND_PROB_ADDITIVE (#1293) * Add lemma prob_div_mul_relf, refactor code, including BAYES_THEOREM, and COND_PROB_ADDITIVE * Replace Unicode characters * remove set up of Holscript mode Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/0027639d9586...ba3052854752 To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Chun T. <no...@gi...> - 2024-09-09 01:11:09
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 3f726a4243be5a37ebd3437ceeab9bbafdcb6139 https://github.com/HOL-Theorem-Prover/HOL/commit/3f726a4243be5a37ebd3437ceeab9bbafdcb6139 Author: Chun Tian <bin...@gm...> Date: 2024-09-09 (Mon, 09 Sep 2024) Changed paths: M examples/dependability/AvailabilityScript.sml M examples/dependability/case_studies/WSNScript.sml M examples/dependability/case_studies/smart_gridScript.sml M examples/probability/large_numberScript.sml M src/num/theories/whileScript.sml M src/pred_set/src/more_theories/topologyScript.sml M src/probability/extrealScript.sml M src/probability/martingaleScript.sml M src/probability/probabilityScript.sml M src/real/analysis/derivativeScript.sml M src/real/analysis/integrationScript.sml M src/real/analysis/limScript.sml M src/real/analysis/real_topologyScript.sml M src/real/analysis/seqScript.sml M src/real/metricScript.sml M src/real/netsScript.sml M src/real/realScript.sml Log Message: ----------- Updates to convergence concepts for potential infinite-valued r.v.'s (#1295) * Updates to convergence concepts for potential infinite-valued r.v.'s * Remove unfinished work... * FTBFS * Added missing NUM_FLOOR_POS, etc. in realTheory * FTBFS examples/dependability To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Andreas L. <no...@gi...> - 2024-09-09 01:07:00
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 0f9ee5c92920aa43012234488972292395d373dc https://github.com/HOL-Theorem-Prover/HOL/commit/0f9ee5c92920aa43012234488972292395d373dc Author: Andreas Lindner <an...@kt...> Date: 2024-09-09 (Mon, 09 Sep 2024) Changed paths: M examples/l3-machine-code/riscv/src/riscv.spec Log Message: ----------- Fix bug in L3 spec of RISC-V (JAL and JALR addr alignment) To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Tu P. <no...@gi...> - 2024-09-03 23:01:10
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: ba3052854752b85c309b047ba1e544f17084e071 https://github.com/HOL-Theorem-Prover/HOL/commit/ba3052854752b85c309b047ba1e544f17084e071 Author: Tu Phan <842...@us...> Date: 2024-09-04 (Wed, 04 Sep 2024) Changed paths: M src/probability/probabilityScript.sml Log Message: ----------- Add lemma prob_div_mul_relf, refactor code in proofs of BAYES_THEOREM, and COND_PROB_ADDITIVE (#1293) * Add lemma prob_div_mul_relf, refactor code, including BAYES_THEOREM, and COND_PROB_ADDITIVE * Replace Unicode characters * remove set up of Holscript mode To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Michael N. <no...@gi...> - 2024-09-03 08:31:47
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 4277a75e45fddd77e02c390c8d347b24592f4841 https://github.com/HOL-Theorem-Prover/HOL/commit/4277a75e45fddd77e02c390c8d347b24592f4841 Author: Michael Norrish <mic...@an...> Date: 2024-09-03 (Tue, 03 Sep 2024) Changed paths: M src/IndDef/InductiveDefinition.sml M src/IndDef/selftest.sml Log Message: ----------- Handle schematic inductive definitions better Closes #1296 To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Michael N. <no...@gi...> - 2024-09-03 00:58:50
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 2a72a369a2fafdbbabd97b0dc399a84e0a6fb59f https://github.com/HOL-Theorem-Prover/HOL/commit/2a72a369a2fafdbbabd97b0dc399a84e0a6fb59f Author: Michael Norrish <mic...@an...> Date: 2024-09-03 (Tue, 03 Sep 2024) Changed paths: M examples/lambda/basics/basic_swapScript.sml Log Message: ----------- Fix regression by removing unnecessary dependency on cardinalTheory The presence of cardinalTheory as an ancestor of lambda/basics/basic_swap caused a later definition that referred to ≼ to imagine that symbol referred to cardinalTheory's cardleq constant rather than listTheory's isPREFIX. Commit: 9e00c4ce6fbc07a18d373d48d2aae2f296dbfe89 https://github.com/HOL-Theorem-Prover/HOL/commit/9e00c4ce6fbc07a18d373d48d2aae2f296dbfe89 Author: Michael Norrish <mic...@an...> Date: 2024-09-03 (Tue, 03 Sep 2024) Changed paths: M examples/computability/kolmog/boolListsScript.sml Log Message: ----------- Modernise some syntax Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/ec4a75e0e390...9e00c4ce6fbc To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Michael N. <no...@gi...> - 2024-09-02 02:29:45
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: ec4a75e0e390ced38f833ea0bf0b90f8cd66073d https://github.com/HOL-Theorem-Prover/HOL/commit/ec4a75e0e390ced38f833ea0bf0b90f8cd66073d Author: Michael Norrish <mic...@an...> Date: 2024-09-02 (Mon, 02 Sep 2024) Changed paths: M Manual/Developers/developers.md Log Message: ----------- Document unicode-grep in Developers' manual To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Michael N. <no...@gi...> - 2024-09-02 02:20:09
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 3cb0aba4cedc178295854e32fa5081b3394d5249 https://github.com/HOL-Theorem-Prover/HOL/commit/3cb0aba4cedc178295854e32fa5081b3394d5249 Author: Michael Norrish <mic...@an...> Date: 2024-09-02 (Mon, 02 Sep 2024) Changed paths: M Manual/Developers/developers.md Log Message: ----------- Minor additions to developers manual. To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Michael N. <no...@gi...> - 2024-09-02 02:00:04
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 0b23319c8ecc906f21d2a366c025d7a6594ee2ea https://github.com/HOL-Theorem-Prover/HOL/commit/0b23319c8ecc906f21d2a366c025d7a6594ee2ea Author: Michael Norrish <mic...@an...> Date: 2024-09-02 (Mon, 02 Sep 2024) Changed paths: M Manual/Developers/developers.md Log Message: ----------- Document source code requirements in the Developers' manual To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Chun T. <no...@gi...> - 2024-09-02 01:41:12
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: d77fa087cdf0dd5088735107607e79ebeaadbe84 https://github.com/HOL-Theorem-Prover/HOL/commit/d77fa087cdf0dd5088735107607e79ebeaadbe84 Author: Chun Tian <bin...@gm...> Date: 2024-09-02 (Mon, 02 Sep 2024) Changed paths: M examples/CCS/CongruenceScript.sml M examples/CCS/ExampleScript.sml M examples/CCS/selftest.sml M examples/lambda/Holmakefile M examples/lambda/barendregt/boehmScript.sml M examples/lambda/barendregt/chap3Script.sml M examples/lambda/barendregt/finite_developmentsScript.sml M examples/lambda/barendregt/head_reductionScript.sml M examples/lambda/barendregt/normal_orderScript.sml M examples/lambda/barendregt/solvableScript.sml M examples/lambda/barendregt/standardisationScript.sml M examples/lambda/basics/Holmakefile M examples/lambda/basics/appFOLDLScript.sml M examples/lambda/basics/basic_swapScript.sml M examples/lambda/basics/generic_termsScript.sml M examples/lambda/basics/nomdatatype.sml M examples/lambda/basics/nomsetScript.sml M examples/lambda/basics/termScript.sml R examples/lambda/completeness/Holmakefile M src/list/src/listRangeScript.sml M src/list/src/listScript.sml M src/list/src/rich_listScript.sml M src/string/stringScript.sml Log Message: ----------- [lambda] Rank-based fresh name allocations; stage work on boehmTheory Commit: 0619699bbfe8a41cae9cf23afe8ca39c42aae11f https://github.com/HOL-Theorem-Prover/HOL/commit/0619699bbfe8a41cae9cf23afe8ca39c42aae11f Author: Chun Tian <bin...@gm...> Date: 2024-09-02 (Mon, 02 Sep 2024) Changed paths: M examples/lambda/barendregt/boehmScript.sml Log Message: ----------- Removed wrongly committed dead code Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/6b42bd1b3a87...0619699bbfe8 To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Chun T. <no...@gi...> - 2024-09-02 01:39:28
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 6b42bd1b3a874b4ff6e94f45a6082300742bc1a7 https://github.com/HOL-Theorem-Prover/HOL/commit/6b42bd1b3a874b4ff6e94f45a6082300742bc1a7 Author: Chun Tian <bin...@gm...> Date: 2024-09-02 (Mon, 02 Sep 2024) Changed paths: M examples/probability/stochastic_processScript.sml M src/probability/borelScript.sml M src/probability/probabilityScript.sml M src/probability/sigma_algebraScript.sml Log Message: ----------- Infinite-dimensional Borel space To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: gengarrrr <no...@gi...> - 2024-09-02 01:38:25
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: bfe9f788ddcd0cee9e70b1d672160f01ff10ab00 https://github.com/HOL-Theorem-Prover/HOL/commit/bfe9f788ddcd0cee9e70b1d672160f01ff10ab00 Author: gengarrrr <104...@us...> Date: 2024-09-02 (Mon, 02 Sep 2024) Changed paths: M examples/Crypto/DES/des_propScript.sml Log Message: ----------- Update des_propScript.sml To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Michael N. <no...@gi...> - 2024-08-30 04:57:14
|
Branch: refs/heads/master Home: https://github.com/HOL-Theorem-Prover/HOL Commit: aaa51b33c6cb44514a0f7f45f846c596f7df9640 https://github.com/HOL-Theorem-Prover/HOL/commit/aaa51b33c6cb44514a0f7f45f846c596f7df9640 Author: Michael Norrish <mic...@an...> Date: 2024-08-29 (Thu, 29 Aug 2024) Changed paths: M tools/hol-mode.src M tools/holscript-mode.el Log Message: ----------- [emacs-mode] Fix modes to properly support modern Quote syntax Commit: 993e2b793c4806b95edbe6546cb59f71e30e84da https://github.com/HOL-Theorem-Prover/HOL/commit/993e2b793c4806b95edbe6546cb59f71e30e84da Author: Michael Norrish <mic...@an...> Date: 2024-08-29 (Thu, 29 Aug 2024) Changed paths: M examples/fun-op-sem/cbv-lc/typesScript.sml Log Message: ----------- [examples/fun-op-sem] modernise syntax in SN for CBV λ-calc. proof Commit: 0027639d9586b620303c54f45954b93896dd4587 https://github.com/HOL-Theorem-Prover/HOL/commit/0027639d9586b620303c54f45954b93896dd4587 Author: Michael Norrish <mic...@an...> Date: 2024-08-29 (Thu, 29 Aug 2024) Changed paths: M tools/hol-mode.src Log Message: ----------- [emacs-mode] Fix error in detection of structures caused by previous Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/de7fb61814ac...0027639d9586 To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |