Session Separation_Algebra
View
theory dependencies
View
document
View
outline
Theories
HOL-Hoare.Hoare_Syntax
File ‹hoare_syntax.ML›
HOL-Hoare.Hoare_Tac
File ‹hoare_tac.ML›
HOL-Hoare.Hoare_Logic_Abort
Separation_Algebra
Sep_Heap_Instance
Sep_Tactics
File ‹sep_tactics.ML›
Simple_Separation_Example
Sep_Tactics_Test
Map_Extra
VM_Example
Separation_Algebra_Alt
Sep_Eq
HOL-Library.Phantom_Type
HOL-Library.Cardinality
HOL-Library.Numeral_Type
HOL-Library.Type_Length
HOL-Library.Word
File ‹Tools/word_lib.ML›
File ‹Tools/smt_word.ML›
Types_D
Abstract_Separation_D
Separation_D