-
e41142896f
Proved basic properties of Blanchet protocol
main
Your Name
2026-03-11 17:11:44 +01:00
-
c705c80f23
Replaced some cases instances with grind
Your Name
2026-03-05 10:02:06 +01:00
-
80db88efbe
Added expand_parts_element macro
Your Name
2026-03-04 18:44:21 +01:00
-
7367681bc6
Simplified proofs in NS_Public
Your Name
2026-03-04 00:56:37 +01:00
-
96e5d59603
Finished proff of NS
Your Name
2026-02-25 17:27:16 +01:00
-
31e638dd90
Translated library, started to prove NS_Public
Your Name
2026-02-23 09:06:13 +01:00
-
61616dc3b1
Translated library Event
Your Name
2026-01-17 10:46:31 +01:00
-
2c7e00905a
Translated Paulson's Message library
Your Name
2026-01-15 15:34:14 +01:00
-
87e50259d3
feat: neue Datentypen für Nachrichten und deren Eigenschaften hinzufügen
Your Name
2025-09-22 11:49:06 +02:00
-
3f5c7807f3
feat: Übersetze Isabelle-Datentyp Agent nach Lean4 als induktiven Typ
Your Name
2025-09-22 11:48:42 +02:00
-
f25a2dda4e
Set up project
Leopold Fajtak
2025-09-22 09:56:03 +02:00