--- a/src/HOL/Hoare/Separation.thy Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Separation.thy Wed Dec 23 22:25:22 2020 +0100
@@ -9,10 +9,13 @@
into parser and pretty printer, which is not very modular.
Alternative: some syntax like <P> which stands for P H. No more
compact, but avoids the funny H.
-
*)
-theory Separation imports Hoare_Logic_Abort SepLogHeap begin
+section \<open>Separation logic\<close>
+
+theory Separation
+ imports Hoare_Logic_Abort SepLogHeap
+begin
text\<open>The semantic definition of a few connectives:\<close>