-
examples!8
-
examples!9
-
Logically atomic triples: Notation, tactics, small example 3 of 3 checklist items completediris!163
-
Super `iModIntro` tactic that generalizes `iAlways`, `iNext`, `iModIntro`, and more 7 of 7 checklist items completediris!121 gen_proofmode
-
iris!174 iris-3.1
-
iris!180
-
iris!176 mtac2-tt
-
iris!173
-
iris!161 gen_proofmode
-
Fine-grained post-conditions for forked-off threads 2 of 2 checklist items completediris!182