-
Slightly weaker WP (i.e., easier to prove), so that we have an fupd where we did not 1 of 1 checklist item completediris!153 gen_proofmode
-
stdpp!35
-
stdpp!36
-
Implement modular specifications from the HOCAP paper 3 of 3 checklist items completedexamples!5