Theory Separation_Logic_Imperative_HOL.Sep_Main

section ‹Separation Logic Framework Entrypoint›
theory Sep_Main
imports Automation
begin
  text ‹Import this theory to make available Imperative/HOL with 
    separation logic.›
end