-
stdpp!39
-
stdpp!40
-
iris!66
-
iris!116 gen_proofmode
-
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