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
(33) |
Oct
(44) |
Nov
|
Dec
|
From: Ramana K. <no...@gi...> - 2024-10-16 11:24:58
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 592eb5e5142344393229eb9777aa198a4b8e152b https://github.com/HOL-Theorem-Prover/HOL/commit/592eb5e5142344393229eb9777aa198a4b8e152b Author: Ramana Kumar <ra...@me...> Date: 2024-10-16 (Wed, 16 Oct 2024) Changed paths: M src/pred_set/src/more_theories/finite_setScript.sml Log Message: ----------- Add some theorems to finite_setTheory (#1320) * Add some theorems to finite_setTheory * Remove fIMAGE_MAP (redundant) 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-10-16 11:24:56
|
Branch: refs/heads/fset Home: https://github.com/HOL-Theorem-Prover/HOL To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Ramana K. <no...@gi...> - 2024-10-16 07:15:20
|
Branch: refs/heads/fset Home: https://github.com/HOL-Theorem-Prover/HOL Commit: df655ec1315a7e1d4416110d258dc51cd9435a88 https://github.com/HOL-Theorem-Prover/HOL/commit/df655ec1315a7e1d4416110d258dc51cd9435a88 Author: Ramana Kumar <ra...@me...> Date: 2024-10-16 (Wed, 16 Oct 2024) Changed paths: M src/pred_set/src/more_theories/finite_setScript.sml Log Message: ----------- Remove fIMAGE_MAP (redundant) 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-10-16 02:35:21
|
Branch: refs/heads/while Home: https://github.com/HOL-Theorem-Prover/HOL To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Ramana K. <no...@gi...> - 2024-10-16 02:35:12
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: f7ad0d96f46fc16085729463a47a75a3395d7bda https://github.com/HOL-Theorem-Prover/HOL/commit/f7ad0d96f46fc16085729463a47a75a3395d7bda Author: Ramana Kumar <ra...@me...> Date: 2024-10-16 (Wed, 16 Oct 2024) Changed paths: M examples/Crypto/Keccak/keccakScript.sml M src/num/theories/arithmeticScript.sml M src/num/theories/whileScript.sml Log Message: ----------- Move some theorems out of keccakScript.sml To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: rsoeldner <no...@gi...> - 2024-10-16 02:28:04
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 5c95ae60327ece0c3036c5eea0a4f2cd450c5cc5 https://github.com/HOL-Theorem-Prover/HOL/commit/5c95ae60327ece0c3036c5eea0a4f2cd450c5cc5 Author: Robert Soeldner <r.s...@gm...> Date: 2024-10-16 (Wed, 16 Oct 2024) Changed paths: M examples/json/Json.sig M examples/json/Json.sml Log Message: ----------- add getKeys to json lib 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-10-16 02:08:42
|
Branch: refs/heads/master Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 43c3c1f2878821a0b42abb4bf7b37a35174be14f https://github.com/HOL-Theorem-Prover/HOL/commit/43c3c1f2878821a0b42abb4bf7b37a35174be14f Author: Michael Norrish <mic...@an...> Date: 2024-10-15 (Tue, 15 Oct 2024) Changed paths: M examples/cv_compute/Holmakefile A examples/cv_compute/soundness_check/cv_compute_unsoundScript.sml M src/thm/otknl-thm.ML M src/thm/std-thm.ML Log Message: ----------- Fix for a soundness bug in cv-compute found by Ramana Kumar His demonstration file is included in the examples/cv_compute/soundness_check directory and there is machinery in the Holmakefile to check that its attempt to prove false (now) fails. Commit: b345eaf500ac23b1db6f4114235fd39e809818ca https://github.com/HOL-Theorem-Prover/HOL/commit/b345eaf500ac23b1db6f4114235fd39e809818ca Author: Michael Norrish <mic...@an...> Date: 2024-10-15 (Tue, 15 Oct 2024) Changed paths: M tools/Holmake/QFRead.sml M tools/Holmake/tests/parallel_tests/Holmakefile A tools/Holmake/tests/use-fnf/Holmakefile A tools/Holmake/tests/use-fnf/test.ML Log Message: ----------- Stop QFRead from killing whole process on a file-not-found Thanks to Discord's shuhan for the bug report. With a test-case in tools/Holmake/tests/use-fnf Commit: 07c84bff2b89ddb2c81c57884f4141bbc37accdb https://github.com/HOL-Theorem-Prover/HOL/commit/07c84bff2b89ddb2c81c57884f4141bbc37accdb Author: Michael Norrish <mic...@an...> Date: 2024-10-15 (Tue, 15 Oct 2024) Changed paths: M examples/cv_compute/Holmakefile Log Message: ----------- Fix cv_compute regression test to cope with case-sensitive files Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/a62035f0f999...07c84bff2b89 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-10-16 01:10:37
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 29bcfcf9503582bc9b97d097a702ede6460bc3b5 https://github.com/HOL-Theorem-Prover/HOL/commit/29bcfcf9503582bc9b97d097a702ede6460bc3b5 Author: Michael Norrish <mic...@an...> Date: 2024-10-16 (Wed, 16 Oct 2024) Changed paths: M examples/cv_compute/Holmakefile R examples/cv_compute/soundness_check/cv_compute_unsoundScript.sml A src/num/theories/cv_compute/soundness_check/Holmakefile A src/num/theories/cv_compute/soundness_check/cv_compute_unsoundScript.sml A src/num/theories/cv_compute/soundness_check/selftest.sml M tools/sequences/core-theories Log Message: ----------- Move cv-compute test to earlier in build; make it more specific 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-10-15 05:31:10
|
Branch: refs/heads/master Home: https://github.com/HOL-Theorem-Prover/HOL Commit: daa2baba20e74ed8be09481326c91b3576c913d9 https://github.com/HOL-Theorem-Prover/HOL/commit/daa2baba20e74ed8be09481326c91b3576c913d9 Author: Ramana Kumar <ra...@me...> Date: 2024-10-10 (Thu, 10 Oct 2024) Changed paths: M src/finite_maps/sptreeScript.sml M src/num/theories/cv_compute/automation/cv_stdScript.sml M src/pred_set/src/more_theories/finite_setScript.sml Log Message: ----------- Add cv support for finite sets of nums (#1318) * Add theorem: wf_list_to_num_set * Add theorem: MEM_fset_REP * Add support for num fset to cv_stdTheory Not all operations are included here, but it's enough to get going with. * Use Num 0 instead of from_unit () in cv_rep thm * Add cv_rep for fEMPTY: num_set * Add cv_rep for fUNION and fset_ABS for num fsets Commit: 03e6a40667959b02507c9f9d9e207e02ffebc912 https://github.com/HOL-Theorem-Prover/HOL/commit/03e6a40667959b02507c9f9d9e207e02ffebc912 Author: Michael Norrish <mic...@an...> Date: 2024-10-11 (Fri, 11 Oct 2024) Changed paths: M Manual/Description/description.tex Log Message: ----------- DESCRIPTION: index "modern syntax" Commit: f594dd77be1a19765f1512f65c38b1e8378feff9 https://github.com/HOL-Theorem-Prover/HOL/commit/f594dd77be1a19765f1512f65c38b1e8378feff9 Author: Konrad Slind <kon...@gm...> Date: 2024-10-12 (Sat, 12 Oct 2024) Changed paths: M examples/formal-languages/FormalLangScript.sml M examples/formal-languages/regular/regularScript.sml Log Message: ----------- Incremental progress towards equivalence of regular languages and finite state languages Commit: 09787b0e172ef82d2b59433cfec29aae9accb348 https://github.com/HOL-Theorem-Prover/HOL/commit/09787b0e172ef82d2b59433cfec29aae9accb348 Author: Konrad Slind <kon...@gm...> Date: 2024-10-12 (Sat, 12 Oct 2024) Changed paths: A examples/json/Json.sig A examples/json/Json.sml A examples/json/README Log Message: ----------- Bare bones JSON parser and prettyprinter. Commit: 9ee2f8682bb3bb6816133dc78e0cb82f600ee53a https://github.com/HOL-Theorem-Prover/HOL/commit/9ee2f8682bb3bb6816133dc78e0cb82f600ee53a Author: Michael Norrish <mic...@an...> Date: 2024-10-14 (Mon, 14 Oct 2024) Changed paths: M examples/json/Json.sig M examples/json/Json.sml Log Message: ----------- Cleanup character-encoding, TABs and trailing whitespace in Json Commit: 49aeab49b79500cd1e004a1b75ee1553495ffee7 https://github.com/HOL-Theorem-Prover/HOL/commit/49aeab49b79500cd1e004a1b75ee1553495ffee7 Author: Robert Soeldner <r.s...@gm...> Date: 2024-10-14 (Mon, 14 Oct 2024) Changed paths: M examples/json/Json.sig M examples/json/Json.sml Log Message: ----------- add basic json accessors Commit: a62035f0f9996617ea9f6f0da49d8c3ce11b509d https://github.com/HOL-Theorem-Prover/HOL/commit/a62035f0f9996617ea9f6f0da49d8c3ce11b509d Author: Konrad Slind <kon...@gm...> Date: 2024-10-14 (Mon, 14 Oct 2024) Changed paths: M examples/json/Json.sig M examples/json/Json.sml Log Message: ----------- Merge pull request #1322 from rsoeldner/json-accessors add basic json accessors Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/4d1b16443810...a62035f0f999 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-10-15 03:21:40
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 07c84bff2b89ddb2c81c57884f4141bbc37accdb https://github.com/HOL-Theorem-Prover/HOL/commit/07c84bff2b89ddb2c81c57884f4141bbc37accdb Author: Michael Norrish <mic...@an...> Date: 2024-10-15 (Tue, 15 Oct 2024) Changed paths: M examples/cv_compute/Holmakefile Log Message: ----------- Fix cv_compute regression test to cope with case-sensitive files 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-10-15 00:20:05
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 43c3c1f2878821a0b42abb4bf7b37a35174be14f https://github.com/HOL-Theorem-Prover/HOL/commit/43c3c1f2878821a0b42abb4bf7b37a35174be14f Author: Michael Norrish <mic...@an...> Date: 2024-10-15 (Tue, 15 Oct 2024) Changed paths: M examples/cv_compute/Holmakefile A examples/cv_compute/soundness_check/cv_compute_unsoundScript.sml M src/thm/otknl-thm.ML M src/thm/std-thm.ML Log Message: ----------- Fix for a soundness bug in cv-compute found by Ramana Kumar His demonstration file is included in the examples/cv_compute/soundness_check directory and there is machinery in the Holmakefile to check that its attempt to prove false (now) fails. Commit: b345eaf500ac23b1db6f4114235fd39e809818ca https://github.com/HOL-Theorem-Prover/HOL/commit/b345eaf500ac23b1db6f4114235fd39e809818ca Author: Michael Norrish <mic...@an...> Date: 2024-10-15 (Tue, 15 Oct 2024) Changed paths: M tools/Holmake/QFRead.sml M tools/Holmake/tests/parallel_tests/Holmakefile A tools/Holmake/tests/use-fnf/Holmakefile A tools/Holmake/tests/use-fnf/test.ML Log Message: ----------- Stop QFRead from killing whole process on a file-not-found Thanks to Discord's shuhan for the bug report. With a test-case in tools/Holmake/tests/use-fnf Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/a62035f0f999...b345eaf500ac 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-10-14 21:25:18
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 49aeab49b79500cd1e004a1b75ee1553495ffee7 https://github.com/HOL-Theorem-Prover/HOL/commit/49aeab49b79500cd1e004a1b75ee1553495ffee7 Author: Robert Soeldner <r.s...@gm...> Date: 2024-10-14 (Mon, 14 Oct 2024) Changed paths: M examples/json/Json.sig M examples/json/Json.sml Log Message: ----------- add basic json accessors Commit: a62035f0f9996617ea9f6f0da49d8c3ce11b509d https://github.com/HOL-Theorem-Prover/HOL/commit/a62035f0f9996617ea9f6f0da49d8c3ce11b509d Author: Konrad Slind <kon...@gm...> Date: 2024-10-14 (Mon, 14 Oct 2024) Changed paths: M examples/json/Json.sig M examples/json/Json.sml Log Message: ----------- Merge pull request #1322 from rsoeldner/json-accessors add basic json accessors Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/9ee2f8682bb3...a62035f0f999 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-10-14 04:42:31
|
Branch: refs/heads/located_thms Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 06e3157b71fd803ab9a879cfbbbc5d819600d810 https://github.com/HOL-Theorem-Prover/HOL/commit/06e3157b71fd803ab9a879cfbbbc5d819600d810 Author: Michael Norrish <mic...@an...> Date: 2024-10-14 (Mon, 14 Oct 2024) Changed paths: M developers/datfile-format.md M src/1/boolLib.sml M src/postkernel/DB.sig M src/postkernel/DB.sml M src/postkernel/DB_dtype.sml M src/postkernel/SharingTables.sml M src/postkernel/Theory.sml M src/postkernel/TheoryDelta.sml M src/postkernel/TheoryPP.sig M src/postkernel/TheoryPP.sml M src/postkernel/TheoryReader.sml Log Message: ----------- Simplify code by moving thm-classes into DB's thminfo type The data format gets simpler too. 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-10-14 02:45:42
|
Branch: refs/heads/located_thms Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 2d44df4caaa33bfd16e9fcf933c62cd8ab60d748 https://github.com/HOL-Theorem-Prover/HOL/commit/2d44df4caaa33bfd16e9fcf933c62cd8ab60d748 Author: Michael Norrish <mic...@an...> Date: 2024-10-14 (Mon, 14 Oct 2024) Changed paths: M tools/Holmake/QuoteFilter M tools/Holmake/tests/quote-filter/expected-mosml M tools/Holmake/tests/quote-filter/expected-poly M tools/Holmake/tests/quote-filter/input Log Message: ----------- Add #(LINE) as a "macro" in QuoteFilter to return current linenumber Won't work well interactively if cut-and-pasting from an editor buffer, but intention is that this should only be used in relatively rare cases. Commit: fc6f440f64ba00140becf805b1919a6c68b189cd https://github.com/HOL-Theorem-Prover/HOL/commit/fc6f440f64ba00140becf805b1919a6c68b189cd Author: Michael Norrish <mic...@an...> Date: 2024-10-14 (Mon, 14 Oct 2024) Changed paths: M developers/datfile-format.md M src/1/DiskThms.sml M src/1/boolLib.sml M src/bool/boolScript.sml M src/postkernel/DB.sig M src/postkernel/DB.sml M src/postkernel/DB_dtype.sml M src/postkernel/SharingTables.sig M src/postkernel/SharingTables.sml M src/postkernel/Theory.sig M src/postkernel/Theory.sml M src/postkernel/TheoryDelta.sml M src/postkernel/TheoryPP.sig M src/postkernel/TheoryPP.sml M src/postkernel/TheoryReader.sig M src/postkernel/TheoryReader.sml Log Message: ----------- Implement theorem locations At the lowest, "kernel" level, the user is responsible for attaching these via the gen_{save_thm,...} entrypoints. Interactively, these can be recovered from the DB; they are stored and loaded in the .dat files. Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/2d44df4caaa3%5E...fc6f440f64ba 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-10-13 23:27:18
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 9ee2f8682bb3bb6816133dc78e0cb82f600ee53a https://github.com/HOL-Theorem-Prover/HOL/commit/9ee2f8682bb3bb6816133dc78e0cb82f600ee53a Author: Michael Norrish <mic...@an...> Date: 2024-10-14 (Mon, 14 Oct 2024) Changed paths: M examples/json/Json.sig M examples/json/Json.sml Log Message: ----------- Cleanup character-encoding, TABs and trailing whitespace in Json To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Ramana K. <no...@gi...> - 2024-10-12 10:07:59
|
Branch: refs/heads/fset Home: https://github.com/HOL-Theorem-Prover/HOL Commit: be2ef4c9a1f1b032f7fa9e55e4c02b7fa7ae8d99 https://github.com/HOL-Theorem-Prover/HOL/commit/be2ef4c9a1f1b032f7fa9e55e4c02b7fa7ae8d99 Author: Ramana Kumar <ra...@me...> Date: 2024-10-12 (Sat, 12 Oct 2024) Changed paths: M src/pred_set/src/more_theories/finite_setScript.sml Log Message: ----------- Add some theorems to finite_setTheory To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Ramana K. <no...@gi...> - 2024-10-12 09:42:36
|
Branch: refs/heads/while Home: https://github.com/HOL-Theorem-Prover/HOL Commit: fa426454ff1bb0c43b8acffdadd4720fccf85706 https://github.com/HOL-Theorem-Prover/HOL/commit/fa426454ff1bb0c43b8acffdadd4720fccf85706 Author: Ramana Kumar <ra...@me...> Date: 2024-10-12 (Sat, 12 Oct 2024) Changed paths: M examples/Crypto/Keccak/keccakScript.sml M src/num/theories/arithmeticScript.sml M src/num/theories/whileScript.sml Log Message: ----------- Move some theorems out of keccakScript.sml 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-10-12 08:19:41
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 09787b0e172ef82d2b59433cfec29aae9accb348 https://github.com/HOL-Theorem-Prover/HOL/commit/09787b0e172ef82d2b59433cfec29aae9accb348 Author: Konrad Slind <kon...@gm...> Date: 2024-10-12 (Sat, 12 Oct 2024) Changed paths: A examples/json/Json.sig A examples/json/Json.sml A examples/json/README Log Message: ----------- Bare bones JSON parser and prettyprinter. 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-10-12 08:18:05
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: f594dd77be1a19765f1512f65c38b1e8378feff9 https://github.com/HOL-Theorem-Prover/HOL/commit/f594dd77be1a19765f1512f65c38b1e8378feff9 Author: Konrad Slind <kon...@gm...> Date: 2024-10-12 (Sat, 12 Oct 2024) Changed paths: M examples/formal-languages/FormalLangScript.sml M examples/formal-languages/regular/regularScript.sml Log Message: ----------- Incremental progress towards equivalence of regular languages and finite state languages 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-10-11 06:02:01
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 03e6a40667959b02507c9f9d9e207e02ffebc912 https://github.com/HOL-Theorem-Prover/HOL/commit/03e6a40667959b02507c9f9d9e207e02ffebc912 Author: Michael Norrish <mic...@an...> Date: 2024-10-11 (Fri, 11 Oct 2024) Changed paths: M Manual/Description/description.tex Log Message: ----------- DESCRIPTION: index "modern syntax" To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Ramana K. <no...@gi...> - 2024-10-11 00:11:37
|
Branch: refs/heads/master Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 7ea8c846eb2869b08689d59331c702388aaafcc5 https://github.com/HOL-Theorem-Prover/HOL/commit/7ea8c846eb2869b08689d59331c702388aaafcc5 Author: Michael Norrish <mic...@an...> Date: 2024-10-04 (Fri, 04 Oct 2024) Changed paths: M tools/editor-modes/emacs/holscript-mode.el M tools/editor-modes/emacs/mode-tests/holscript-tests.el M tools/editor-modes/emacs/mode-tests/sampleScript.sml Log Message: ----------- [emacs-mode] Fix keyword spotting for CoInductive (looking back) Commit: 6b163b4ea75e05d08618ee24f84bc90db896e6aa https://github.com/HOL-Theorem-Prover/HOL/commit/6b163b4ea75e05d08618ee24f84bc90db896e6aa Author: Michael Norrish <mic...@an...> Date: 2024-10-04 (Fri, 04 Oct 2024) Changed paths: M tools/editor-modes/emacs/holscript-mode.el M tools/editor-modes/emacs/yasnippets/holscript-mode/Cases M tools/editor-modes/emacs/yasnippets/holscript-mode/Cases_on M tools/editor-modes/emacs/yasnippets/holscript-mode/Definition M tools/editor-modes/emacs/yasnippets/holscript-mode/Induct M tools/editor-modes/emacs/yasnippets/holscript-mode/Induct_on M tools/editor-modes/emacs/yasnippets/holscript-mode/Theorem M tools/editor-modes/emacs/yasnippets/holscript-mode/metis_tac M tools/editor-modes/emacs/yasnippets/holscript-mode/once_rewrite_tac M tools/editor-modes/emacs/yasnippets/holscript-mode/qpat_x_assum M tools/editor-modes/emacs/yasnippets/holscript-mode/qspecl_then M tools/editor-modes/emacs/yasnippets/holscript-mode/resolve M tools/editor-modes/emacs/yasnippets/holscript-mode/sg Log Message: ----------- [emacs-mode] enable yas-snippets for holscript mode more readily Also adjust some of the snippets for more modern syntax. Commit: 8554cee829b3ebc01d46b592149724efcc49354f https://github.com/HOL-Theorem-Prover/HOL/commit/8554cee829b3ebc01d46b592149724efcc49354f Author: Michael Norrish <mic...@an...> Date: 2024-10-09 (Wed, 09 Oct 2024) Changed paths: A developers/datfile-format.md Log Message: ----------- Document our current .dat format This is a prelude to changing it to incorporate theorem location information. Commit: 4d1b16443810923d9832780d757d1b868bc9eef4 https://github.com/HOL-Theorem-Prover/HOL/commit/4d1b16443810923d9832780d757d1b868bc9eef4 Author: Ramana Kumar <ra...@me...> Date: 2024-10-09 (Wed, 09 Oct 2024) Changed paths: M src/num/theories/cv_compute/automation/cv_typeLib.sml Log Message: ----------- cv translator: allow known fun types in ctors Compare: https://github.com/HOL-Theorem-Prover/HOL/compare/277f6ad61861...4d1b16443810 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-10-10 00:28:32
|
Branch: refs/heads/cv_num_fset Home: https://github.com/HOL-Theorem-Prover/HOL To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Ramana K. <no...@gi...> - 2024-10-10 00:28:28
|
Branch: refs/heads/develop Home: https://github.com/HOL-Theorem-Prover/HOL Commit: daa2baba20e74ed8be09481326c91b3576c913d9 https://github.com/HOL-Theorem-Prover/HOL/commit/daa2baba20e74ed8be09481326c91b3576c913d9 Author: Ramana Kumar <ra...@me...> Date: 2024-10-10 (Thu, 10 Oct 2024) Changed paths: M src/finite_maps/sptreeScript.sml M src/num/theories/cv_compute/automation/cv_stdScript.sml M src/pred_set/src/more_theories/finite_setScript.sml Log Message: ----------- Add cv support for finite sets of nums (#1318) * Add theorem: wf_list_to_num_set * Add theorem: MEM_fset_REP * Add support for num fset to cv_stdTheory Not all operations are included here, but it's enough to get going with. * Use Num 0 instead of from_unit () in cv_rep thm * Add cv_rep for fEMPTY: num_set * Add cv_rep for fUNION and fset_ABS for num fsets To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Ramana K. <no...@gi...> - 2024-10-09 21:57:26
|
Branch: refs/heads/cv_num_fset Home: https://github.com/HOL-Theorem-Prover/HOL Commit: c7b72753bd731bdc7d3e16a2532f0e0d78c5444b https://github.com/HOL-Theorem-Prover/HOL/commit/c7b72753bd731bdc7d3e16a2532f0e0d78c5444b Author: Ramana Kumar <ra...@me...> Date: 2024-10-09 (Wed, 09 Oct 2024) Changed paths: M src/num/theories/cv_compute/automation/cv_stdScript.sml M src/pred_set/src/more_theories/finite_setScript.sml Log Message: ----------- Add cv_rep for fUNION and fset_ABS for num fsets To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |
From: Ramana K. <no...@gi...> - 2024-10-09 21:41:09
|
Branch: refs/heads/cv_num_fset Home: https://github.com/HOL-Theorem-Prover/HOL Commit: 4821902b28d50c57384fa3b2c960040b8a872783 https://github.com/HOL-Theorem-Prover/HOL/commit/4821902b28d50c57384fa3b2c960040b8a872783 Author: Ramana Kumar <ra...@me...> Date: 2024-10-09 (Wed, 09 Oct 2024) Changed paths: M src/num/theories/cv_compute/automation/cv_stdScript.sml Log Message: ----------- Add cv_rep for fEMPTY: num_set To unsubscribe from these emails, change your notification settings at https://github.com/HOL-Theorem-Prover/HOL/settings/notifications |