HOL-Nominal-Examples

Class1

Class2

Class3

CK_Machine

Compile

Contexts

Crary

CR_Takahashi

Lam_Funs

CR

Fsub

Height

Lambda_mu

LocalWeakening

Pattern

SN

SOS

Standardization

Support

Type_Preservation

Weakening

W

VC_Condition