{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":366050418,"defaultBranch":"main","name":"Hybrid-Verification","ownerLogin":"isabelle-utp","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2021-05-10T13:22:51.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/9845947?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1680192669.887451","currentOid":""},"activityList":{"items":[{"before":"71aa153ccfdfafc2cd7f64259543b576b526be30","after":"a37494317830c7a6db09a14414e698d6c77e7028","ref":"refs/heads/main","pushedAt":"2024-04-09T15:48:26.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Metis proof instead of smt for planar flight problem.","shortMessageHtmlLink":"Metis proof instead of smt for planar flight problem."}},{"before":"1ecce830644fd9137cc21622f306fa176497f2dc","after":"71aa153ccfdfafc2cd7f64259543b576b526be30","ref":"refs/heads/main","pushedAt":"2024-04-09T13:34:17.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Fixed proofs as suggested by reviewers.","shortMessageHtmlLink":"Fixed proofs as suggested by reviewers."}},{"before":"8fd8fb41c8cd56c8f8c6500f42784f499198f9b9","after":"1ecce830644fd9137cc21622f306fa176497f2dc","ref":"refs/heads/main","pushedAt":"2024-02-29T14:48:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Adding kleene star laws","shortMessageHtmlLink":"Adding kleene star laws"}},{"before":"bb5e14e9b8af1d9f36e5914460636e505844d527","after":"8fd8fb41c8cd56c8f8c6500f42784f499198f9b9","ref":"refs/heads/main","pushedAt":"2024-02-08T14:19:44.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"simondfoster","name":"Simon Foster","path":"/simondfoster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4542398?s=80&v=4"},"commit":{"message":"Added nicer printing of lens gets, and tidied one of the examples.","shortMessageHtmlLink":"Added nicer printing of lens gets, and tidied one of the examples."}},{"before":"9c2fc4b7d0028a601e1e10dc6bf935abf6d8630d","after":"bb5e14e9b8af1d9f36e5914460636e505844d527","ref":"refs/heads/main","pushedAt":"2024-01-16T11:06:17.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"simondfoster","name":"Simon Foster","path":"/simondfoster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4542398?s=80&v=4"},"commit":{"message":"Additions to pendulum with force example","shortMessageHtmlLink":"Additions to pendulum with force example"}},{"before":"7981dd8beae46d5220b30d5e59a9d5a62ce353f0","after":"9c2fc4b7d0028a601e1e10dc6bf935abf6d8630d","ref":"refs/heads/main","pushedAt":"2024-01-16T11:05:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"simondfoster","name":"Simon Foster","path":"/simondfoster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4542398?s=80&v=4"},"commit":{"message":"Added syntax fix","shortMessageHtmlLink":"Added syntax fix"}},{"before":"e766a6b4744f37e176cd289e9e80120b6238ad81","after":"7981dd8beae46d5220b30d5e59a9d5a62ce353f0","ref":"refs/heads/main","pushedAt":"2024-01-12T11:07:31.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Added flight collision avoidance.","shortMessageHtmlLink":"Added flight collision avoidance."}},{"before":"e9375c6c010245e65fefb99c965a890177639ed8","after":"e766a6b4744f37e176cd289e9e80120b6238ad81","ref":"refs/heads/main","pushedAt":"2023-12-11T14:49:55.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Added glucose monitor example.","shortMessageHtmlLink":"Added glucose monitor example."}},{"before":"c6b893eb66ea9c91f116cd4145367f1b99735a23","after":"e9375c6c010245e65fefb99c965a890177639ed8","ref":"refs/heads/main","pushedAt":"2023-12-10T21:10:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Adding an exmaple for c1_lipschitz.","shortMessageHtmlLink":"Adding an exmaple for c1_lipschitz."}},{"before":"cf97d1f6f5691e15aab9b24bfff87e01a3d77250","after":"c6b893eb66ea9c91f116cd4145367f1b99735a23","ref":"refs/heads/main","pushedAt":"2023-11-09T17:51:10.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Updated README.md","shortMessageHtmlLink":"Updated README.md"}},{"before":"34d2e2ebc629dca6dbdbb3a3b0985606ed9073fd","after":"cf97d1f6f5691e15aab9b24bfff87e01a3d77250","ref":"refs/heads/main","pushedAt":"2023-11-09T16:18:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Deleted extra $ in a problem.","shortMessageHtmlLink":"Deleted extra $ in a problem."}},{"before":"07d46466796efb9faa94ebcf8cc16f934355bb7d","after":"34d2e2ebc629dca6dbdbb3a3b0985606ed9073fd","ref":"refs/heads/main","pushedAt":"2023-09-26T20:14:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Minor editions.","shortMessageHtmlLink":"Minor editions."}},{"before":"faab69a588fc8d7c8439dac7d15b2734d6f4d4f6","after":"07d46466796efb9faa94ebcf8cc16f934355bb7d","ref":"refs/heads/main","pushedAt":"2023-09-25T16:18:18.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Improved rocket description.","shortMessageHtmlLink":"Improved rocket description."}},{"before":"bfa92455a824ca159d48021bb0a73e453b52da24","after":"faab69a588fc8d7c8439dac7d15b2734d6f4d4f6","ref":"refs/heads/main","pushedAt":"2023-09-25T13:08:29.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Improved presentation of rocket and added it and pendulum with force to ROOT.","shortMessageHtmlLink":"Improved presentation of rocket and added it and pendulum with force …"}},{"before":"7aa6a58e057586085f9eb6d646d523c6b7c85cb5","after":"bfa92455a824ca159d48021bb0a73e453b52da24","ref":"refs/heads/main","pushedAt":"2023-09-23T12:22:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Minor fixes following paper.","shortMessageHtmlLink":"Minor fixes following paper."}},{"before":"4ecbbc0061233aae1c29b9437b740e71e7702d10","after":"7aa6a58e057586085f9eb6d646d523c6b7c85cb5","ref":"refs/heads/main","pushedAt":"2023-09-21T16:05:00.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Fixed water tank broken proof.","shortMessageHtmlLink":"Fixed water tank broken proof."}},{"before":"6c3c081482f25c21e23ce27fb6e9971ca1e29d43","after":"4ecbbc0061233aae1c29b9437b740e71e7702d10","ref":"refs/heads/main","pushedAt":"2023-09-21T13:37:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Moved theory lemmas and fixing example.","shortMessageHtmlLink":"Moved theory lemmas and fixing example."}},{"before":"67c060dfa6f27de0757f3f78e5263dd5c7d43698","after":"6c3c081482f25c21e23ce27fb6e9971ca1e29d43","ref":"refs/heads/main","pushedAt":"2023-09-21T01:18:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Added derivative tests, backward diamonds, and rocket example.","shortMessageHtmlLink":"Added derivative tests, backward diamonds, and rocket example."}},{"before":"c7b14bafaabfc32546f82445b9b90f585a5e38ea","after":"67c060dfa6f27de0757f3f78e5263dd5c7d43698","ref":"refs/heads/main","pushedAt":"2023-09-11T15:11:34.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Added definition of backward diamond. Edited ROOT to generate .pdf.","shortMessageHtmlLink":"Added definition of backward diamond. Edited ROOT to generate .pdf."}},{"before":"f608af886e3f843c0fc1030cb77880f5e6d54d68","after":"c7b14bafaabfc32546f82445b9b90f585a5e38ea","ref":"refs/heads/main","pushedAt":"2023-05-01T01:32:37.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Merge branch 'main' of github.com:isabelle-utp/Hybrid-Verification","shortMessageHtmlLink":"Merge branch 'main' of github.com:isabelle-utp/Hybrid-Verification"}},{"before":"68596714d32ceed10c09fbffc6e4c0bbf54dbe4d","after":"f608af886e3f843c0fc1030cb77880f5e6d54d68","ref":"refs/heads/main","pushedAt":"2023-04-28T10:52:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"simondfoster","name":"Simon Foster","path":"/simondfoster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4542398?s=80&v=4"},"commit":{"message":"Tidied up example and finished the overall proof","shortMessageHtmlLink":"Tidied up example and finished the overall proof"}},{"before":"a41545dfe28a8e6d86779792258ee2e5c4a9d84b","after":"68596714d32ceed10c09fbffc6e4c0bbf54dbe4d","ref":"refs/heads/main","pushedAt":"2023-04-27T15:46:16.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"simondfoster","name":"Simon Foster","path":"/simondfoster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4542398?s=80&v=4"},"commit":{"message":"Added trigonometric property and completed the proof","shortMessageHtmlLink":"Added trigonometric property and completed the proof"}},{"before":"8a419ce8733730c366b3520c212923a736773cc8","after":"a41545dfe28a8e6d86779792258ee2e5c4a9d84b","ref":"refs/heads/main","pushedAt":"2023-04-27T08:02:58.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"simondfoster","name":"Simon Foster","path":"/simondfoster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4542398?s=80&v=4"},"commit":{"message":"Managed to prove the main invariant, still struggling with showing this implies the postcondition","shortMessageHtmlLink":"Managed to prove the main invariant, still struggling with showing th…"}},{"before":"82aa7707b3c48eb6bb239138c36d8fb041b6294c","after":"8a419ce8733730c366b3520c212923a736773cc8","ref":"refs/heads/main","pushedAt":"2023-04-27T08:02:30.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"simondfoster","name":"Simon Foster","path":"/simondfoster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4542398?s=80&v=4"},"commit":{"message":"Made the nondeterministic assignment laws easier to prove by using literals instead of expressions","shortMessageHtmlLink":"Made the nondeterministic assignment laws easier to prove by using li…"}},{"before":"f385f7ccfe1cf28b5872026d4a544a40436bbdf5","after":"82aa7707b3c48eb6bb239138c36d8fb041b6294c","ref":"refs/heads/main","pushedAt":"2023-04-25T16:02:52.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"simondfoster","name":"Simon Foster","path":"/simondfoster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4542398?s=80&v=4"},"commit":{"message":"Added the pendulum with force example","shortMessageHtmlLink":"Added the pendulum with force example"}},{"before":"ff9f51e8682fb1a44a69b3d7f6f25a495e5ee991","after":"f385f7ccfe1cf28b5872026d4a544a40436bbdf5","ref":"refs/heads/main","pushedAt":"2023-04-21T13:38:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"simondfoster","name":"Simon Foster","path":"/simondfoster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4542398?s=80&v=4"},"commit":{"message":"Added differentiable laws for sin and cos","shortMessageHtmlLink":"Added differentiable laws for sin and cos"}},{"before":"4ae47ce0045a2efe1f81780c00c7104b1e0e9394","after":"ff9f51e8682fb1a44a69b3d7f6f25a495e5ee991","ref":"refs/heads/main","pushedAt":"2023-04-21T13:37:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"simondfoster","name":"Simon Foster","path":"/simondfoster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4542398?s=80&v=4"},"commit":{"message":"Added pre-simplification of local_flow theorems, as this ensures that ODEs are ordered alphabetically via the substitution simproc","shortMessageHtmlLink":"Added pre-simplification of local_flow theorems, as this ensures that…"}},{"before":"ccc5876d270a436a3c4be8c44932256e5d291cf3","after":"4ae47ce0045a2efe1f81780c00c7104b1e0e9394","ref":"refs/heads/main","pushedAt":"2023-04-17T13:44:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Setup ARCH22 examples for document generation.","shortMessageHtmlLink":"Setup ARCH22 examples for document generation."}},{"before":"4c71b0513f2d338404309c9a2747d423febe9fae","after":"ccc5876d270a436a3c4be8c44932256e5d291cf3","ref":"refs/heads/main","pushedAt":"2023-03-30T17:03:13.608Z","pushType":"push","commitsCount":1,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Removed some warnings.","shortMessageHtmlLink":"Removed some warnings."}},{"before":"9d48238bf619ea695cada997454dd49bf75f5ed4","after":"4c71b0513f2d338404309c9a2747d423febe9fae","ref":"refs/heads/main","pushedAt":"2023-03-30T16:22:19.201Z","pushType":"push","commitsCount":5,"pusher":{"login":"yonoteam","name":"Jonathan Julian Huerta y Munive","path":"/yonoteam","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10053500?s=80&v=4"},"commit":{"message":"Merge branch 'main' into sdf","shortMessageHtmlLink":"Merge branch 'main' into sdf"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAELC0BugA","startCursor":null,"endCursor":null}},"title":"Activity · isabelle-utp/Hybrid-Verification"}