HOL-CSP_OpSem

Introduction

Sliding

Throw

Interrupt

ReadySet

After

AfterExt

AfterTrace

Motivations

OpSemGeneric

OpSemFD

OpSemDT

AfterExtBis

AfterTraceBis

OpSemGenericBis

OpSemFDBis

OpSemDTBis

OpSemFBis

OpSemTBis

NewLaws

Conclusion