Session Algebraic_VCs
View
theory dependencies
View
document
View
outline
Theories
VC_KAT_scratch
VC_KAD_scratch
P2S2R
VC_KAT
VC_KAT_Examples
HOL-Eisbach.Eisbach
File ‹parse_tools.ML›
File ‹method_closure.ML›
File ‹eisbach_rule_insts.ML›
File ‹match_method.ML›
VC_KAT_Examples2
RKAT
RKAT_Models
VC_RKAT
VC_RKAT_Examples
KAD.Domain_Semiring
KAD.Antidomain_Semiring
KAD.Range_Semiring
KAD.Modal_Kleene_Algebra
KAD.Modal_Kleene_Algebra_Models
VC_KAD
VC_KAD_Examples
VC_KAD_Examples2
VC_KAD_dual
VC_KAD_dual_Examples
KAD.Modal_Kleene_Algebra_Applications
VC_KAD_wf
VC_KAD_wf_Examples
Path_Model_Example
HOL-Hoare.Heap
Pointer_Examples
KAD_is_KAT
Domain_Quantale