H
O
L
-
C
S
P
_
O
p
S
em
Introduction
Sliding
Throw
Interrupt
ReadySet
After
AfterExt
AfterTrace
Motivations
OpSemGeneric
OpSemFD
OpSemDT
AfterExtBis
AfterTraceBis
OpSemGenericBis
OpSemFDBis
OpSemDTBis
OpSemFBis
OpSemTBis
NewLaws
Conclusion